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

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

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