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

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

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

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

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

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

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