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

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

State before:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V ((P.not_.imp_ Q.not_).imp_ (Q.imp_ P))
Tactic:
simp only [eval_not, eval_imp]
State after:
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), (¬evalPrime V P → ¬evalPrime V Q) → evalPrime V Q → evalPrime V P

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