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

State before:
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsProof ((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q)))
Tactic:
apply C_18_4 (forall_ v P) P ((forall_ v (P.imp_ Q)).imp_ ((forall_ v P).imp_ (forall_ v Q)))
State after:
case h1
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsReplOfFormulaInFormula (forall_ v P) P ((forall_ v (P.imp_ Q)).imp_ ((forall_ v P).imp_ (forall_ v Q)))
    ((forall_ v (P.imp_ Q)).imp_ (P.imp_ (forall_ v Q)))

case h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsProof ((forall_ v P).iff_ P)

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

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

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

State before:
case h1.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsReplOfFormulaInFormula (forall_ v P) P (forall_ v (P.imp_ Q)) (forall_ v (P.imp_ Q))
Tactic:
apply IsReplOfFormulaInFormula.same_
State after:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ forall_ v (P.imp_ Q) = forall_ v (P.imp_ Q)

State before:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ forall_ v (P.imp_ Q) = forall_ v (P.imp_ Q)
Tactic:
rfl
State after:
no goals

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

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

State before:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsReplOfFormulaInFormula (forall_ v P) P (forall_ v P) P
Tactic:
apply IsReplOfFormulaInFormula.diff_
State after:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ forall_ v P = forall_ v P

case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ P = P

State before:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ forall_ v P = forall_ v P
Tactic:
rfl
State after:
no goals

State before:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ P = P
Tactic:
rfl
State after:
no goals

State before:
case h1.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsReplOfFormulaInFormula (forall_ v P) P (forall_ v Q) (forall_ v Q)
Tactic:
apply IsReplOfFormulaInFormula.same_
State after:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ forall_ v Q = forall_ v Q

State before:
case h1.a.a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ forall_ v Q = forall_ v Q
Tactic:
rfl
State after:
no goals

State before:
case h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsProof ((forall_ v P).iff_ P)
Tactic:
exact T_19_1 P v h1
State after:
no goals

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

State before:
case h3.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsAxiom ((forall_ v (P.imp_ Q)).imp_ ((forall_ v P).imp_ (forall_ v Q)))
Tactic:
apply IsAxiom.pred_1_
State after:
no goals