Theorem: FOL.NV.T_19_TS_21 (FOL/NV/Margaris/Fol.lean)

State before:
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsProof ((forall_ v (P.imp_ Q)).iff_ (P.imp_ (forall_ v Q)))
Tactic:
apply IsDeduct.mp_ ((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q)))
State after:
case a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_ ((forall_ v (P.imp_ Q)).iff_ (P.imp_ (forall_ v Q))))

case a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q)))

State before:
case a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_ ((forall_ v (P.imp_ Q)).iff_ (P.imp_ (forall_ v Q))))
Tactic:
apply IsDeduct.mp_ ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q)))
State after:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).imp_
      (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_ ((forall_ v (P.imp_ Q)).iff_ (P.imp_ (forall_ v Q)))))

case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q)))

State before:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).imp_
      (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_ ((forall_ v (P.imp_ Q)).iff_ (P.imp_ (forall_ v Q)))))
Tactic:
simp only [def_iff_]
State after:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).imp_
      (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_
        (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).and_
          ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))))))

State before:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).imp_
      (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_
        (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).and_
          ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))))))
Tactic:
simp only [def_and_]
State after:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).imp_
      (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_
        (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_
            ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).not_).not_))

State before:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).imp_
      (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_
        (((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q))).imp_
            ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q))).not_).not_))
Tactic:
SC
State after:
no goals

State before:
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((P.imp_ (forall_ v Q)).imp_ (forall_ v (P.imp_ Q)))
Tactic:
exact T_19_TS_21_right P Q v h1
State after:
no goals

State before:
case a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅ ((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q)))
Tactic:
exact T_19_TS_21_left P Q v h1
State after:
no goals