apply IsDeduct.mp_ (P_U.iff_ 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.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).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)