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

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

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