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

State before:
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ P_V
Tactic:
apply IsDeduct.mp_ P_U
State after:
case a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (P_U.imp_ P_V)

case a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ P_U

State before:
case a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (P_U.imp_ P_V)
Tactic:
apply IsDeduct.mp_ (P_U.iff_ P_V)
State after:
case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ ((P_U.iff_ P_V).imp_ (P_U.imp_ P_V))

case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (P_U.iff_ P_V)

State before:
case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ ((P_U.iff_ P_V).imp_ (P_U.imp_ P_V))
Tactic:
simp only [def_iff_]
State after:
case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (((P_U.imp_ P_V).and_ (P_V.imp_ P_U)).imp_ (P_U.imp_ P_V))

State before:
case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (((P_U.imp_ P_V).and_ (P_V.imp_ P_U)).imp_ (P_U.imp_ P_V))
Tactic:
simp only [def_and_]
State after:
case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (((P_U.imp_ P_V).imp_ (P_V.imp_ P_U).not_).not_.imp_ (P_U.imp_ P_V))

State before:
case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (((P_U.imp_ P_V).imp_ (P_V.imp_ P_U).not_).not_.imp_ (P_U.imp_ P_V))
Tactic:
SC
State after:
no goals

State before:
case a.a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ (P_U.iff_ P_V)
Tactic:
apply proof_imp_deduct
State after:
case a.a.h1
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsProof (P_U.iff_ P_V)

State before:
case a.a.h1
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsProof (P_U.iff_ P_V)
Tactic:
exact C_18_3 U V P_U P_V h1 h2
State after:
no goals

State before:
case a
U V P_U P_V : Formula
Δ : Set Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
h3 : IsDeduct Δ P_U
⊢ IsDeduct Δ P_U
Tactic:
exact h3
State after:
no goals