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

State before:
P : Formula
v : VarName
⊢ IsProof ((forall_ v P).imp_ (exists_ v P))
Tactic:
apply deduction_theorem
State after:
case h1
P : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {forall_ v P}) (exists_ v P)

State before:
case h1
P : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {forall_ v P}) (exists_ v P)
Tactic:
simp
State after:
case h1
P : Formula
v : VarName
⊢ IsDeduct {forall_ v P} (exists_ v P)

State before:
case h1
P : Formula
v : VarName
⊢ IsDeduct {forall_ v P} (exists_ v P)
Tactic:
apply existsIntroId
State after:
case h1.h1
P : Formula
v : VarName
⊢ IsDeduct {forall_ v P} P

State before:
case h1.h1
P : Formula
v : VarName
⊢ IsDeduct {forall_ v P} P
Tactic:
apply specId v
State after:
case h1.h1.h1
P : Formula
v : VarName
⊢ IsDeduct {forall_ v P} (forall_ v P)

State before:
case h1.h1.h1
P : Formula
v : VarName
⊢ IsDeduct {forall_ v P} (forall_ v P)
Tactic:
apply IsDeduct.assume_
State after:
case h1.h1.h1.a
P : Formula
v : VarName
⊢ forall_ v P ∈ {forall_ v P}

State before:
case h1.h1.h1.a
P : Formula
v : VarName
⊢ forall_ v P ∈ {forall_ v P}
Tactic:
simp
State after:
no goals