specialize h1_ih_1 h2_left h3_left
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))