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

State before:
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ IsDeduct Δ (fastReplaceFree v t P)
Tactic:
apply IsDeduct.mp_ (forall_ v P)
State after:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ IsDeduct Δ ((forall_ v P).imp_ (fastReplaceFree v t P))

case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ IsDeduct Δ (forall_ v P)

State before:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ IsDeduct Δ ((forall_ v P).imp_ (fastReplaceFree v t P))
Tactic:
apply IsDeduct.axiom_
State after:
case a.a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ IsAxiom ((forall_ v P).imp_ (fastReplaceFree v t P))

State before:
case a.a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ IsAxiom ((forall_ v P).imp_ (fastReplaceFree v t P))
Tactic:
apply IsAxiom.pred_2_ v t P (fastReplaceFree v t P) h2
State after:
case a.a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ fastReplaceFree v t P = fastReplaceFree v t P

State before:
case a.a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ fastReplaceFree v t P = fastReplaceFree v t P
Tactic:
rfl
State after:
no goals

State before:
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
h2 : fastAdmits v t P
⊢ IsDeduct Δ (forall_ v P)
Tactic:
exact h1
State after:
no goals