Theorem: FOL.NV.T_14_9_Deduct (FOL/NV/Margaris/Prop.lean)

State before:
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ P
Tactic:
apply IsDeduct.mp_ (U.not_.imp_ P)
State after:
case a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ ((U.not_.imp_ P).imp_ P)

case a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ (U.not_.imp_ P)

State before:
case a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ ((U.not_.imp_ P).imp_ P)
Tactic:
apply IsDeduct.mp_ (U.imp_ P)
State after:
case a.a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ ((U.imp_ P).imp_ ((U.not_.imp_ P).imp_ P))

case a.a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ (U.imp_ P)

State before:
case a.a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ ((U.imp_ P).imp_ ((U.not_.imp_ P).imp_ P))
Tactic:
apply proof_imp_deduct
State after:
case a.a.h1
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsProof ((U.imp_ P).imp_ ((U.not_.imp_ P).imp_ P))

State before:
case a.a.h1
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsProof ((U.imp_ P).imp_ ((U.not_.imp_ P).imp_ P))
Tactic:
apply T_14_9
State after:
no goals

State before:
case a.a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ (U.imp_ P)
Tactic:
apply deduction_theorem
State after:
case a.a.h1
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct (Δ ∪ {U}) P

State before:
case a.a.h1
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct (Δ ∪ {U}) P
Tactic:
exact h1
State after:
no goals

State before:
case a
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct Δ (U.not_.imp_ P)
Tactic:
apply deduction_theorem
State after:
case a.h1
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct (Δ ∪ {U.not_}) P

State before:
case a.h1
P U : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {U}) P
h2 : IsDeduct (Δ ∪ {U.not_}) P
⊢ IsDeduct (Δ ∪ {U.not_}) P
Tactic:
exact h2
State after:
no goals