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

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

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

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