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

State before:
Q Q' P_u P_v : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (exists_ u P_u) (exists_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsDeduct Δ Q'
Tactic:
apply C_18_4 (exists_ u P_u) (exists_ v P_v) Q Q' Δ h2
State after:
case h2
Q Q' P_u P_v : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (exists_ u P_u) (exists_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsProof ((exists_ u P_u).iff_ (exists_ v P_v))

case h3
Q Q' P_u P_v : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (exists_ u P_u) (exists_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsDeduct Δ Q

State before:
case h2
Q Q' P_u P_v : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (exists_ u P_u) (exists_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsProof ((exists_ u P_u).iff_ (exists_ v P_v))
Tactic:
exact T_18_8 P_u P_v u v h3
State after:
no goals

State before:
case h3
Q Q' P_u P_v : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (exists_ u P_u) (exists_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsDeduct Δ Q
Tactic:
exact h1
State after:
no goals