Theorem: FOL.NV.is_tauto_mp (FOL/NV/Margaris/Prop.lean)

State before:
P Q : Formula
h1 : (P.imp_ Q).IsTautoPrime
h2 : P.IsTautoPrime
⊢ Q.IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime] at h1
State after:
P Q : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V (P.imp_ Q)
h2 : P.IsTautoPrime
⊢ Q.IsTautoPrime

State before:
P Q : Formula
h1 : ∀ (V : VarBoolAssignment), evalPrime V (P.imp_ Q)
h2 : P.IsTautoPrime
⊢ Q.IsTautoPrime
Tactic:
simp only [eval_imp] at h1
State after:
P Q : Formula
h2 : P.IsTautoPrime
h1 : ∀ (V : VarBoolAssignment), evalPrime V P → evalPrime V Q
⊢ Q.IsTautoPrime

State before:
P Q : Formula
h2 : P.IsTautoPrime
h1 : ∀ (V : VarBoolAssignment), evalPrime V P → evalPrime V Q
⊢ Q.IsTautoPrime
Tactic:
simp only [Formula.IsTautoPrime] at h2
State after:
P Q : Formula
h2 : ∀ (V : VarBoolAssignment), evalPrime V P
h1 : ∀ (V : VarBoolAssignment), evalPrime V P → evalPrime V Q
⊢ Q.IsTautoPrime

State before:
P Q : Formula
h2 : ∀ (V : VarBoolAssignment), evalPrime V P
h1 : ∀ (V : VarBoolAssignment), evalPrime V P → evalPrime V Q
⊢ Q.IsTautoPrime
Tactic:
tauto
State after:
no goals