Metamath Proof Explorer


Theorem bi2bian9

Description: Deduction joining two biconditionals with different antecedents. (Contributed by NM, 12-May-2004)

Ref Expression
Hypotheses bi2an9.1 ( 𝜑 → ( 𝜓𝜒 ) )
bi2an9.2 ( 𝜃 → ( 𝜏𝜂 ) )
Assertion bi2bian9 ( ( 𝜑𝜃 ) → ( ( 𝜓𝜏 ) ↔ ( 𝜒𝜂 ) ) )

Proof

Step Hyp Ref Expression
1 bi2an9.1 ( 𝜑 → ( 𝜓𝜒 ) )
2 bi2an9.2 ( 𝜃 → ( 𝜏𝜂 ) )
3 1 adantr ( ( 𝜑𝜃 ) → ( 𝜓𝜒 ) )
4 2 adantl ( ( 𝜑𝜃 ) → ( 𝜏𝜂 ) )
5 3 4 bibi12d ( ( 𝜑𝜃 ) → ( ( 𝜓𝜏 ) ↔ ( 𝜒𝜂 ) ) )