Metamath Proof Explorer


Theorem bi2bian9

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

Ref Expression
Hypotheses bi2an9.1
|- ( ph -> ( ps <-> ch ) )
bi2an9.2
|- ( th -> ( ta <-> et ) )
Assertion bi2bian9
|- ( ( ph /\ th ) -> ( ( ps <-> ta ) <-> ( ch <-> et ) ) )

Proof

Step Hyp Ref Expression
1 bi2an9.1
 |-  ( ph -> ( ps <-> ch ) )
2 bi2an9.2
 |-  ( th -> ( ta <-> et ) )
3 1 adantr
 |-  ( ( ph /\ th ) -> ( ps <-> ch ) )
4 2 adantl
 |-  ( ( ph /\ th ) -> ( ta <-> et ) )
5 3 4 bibi12d
 |-  ( ( ph /\ th ) -> ( ( ps <-> ta ) <-> ( ch <-> et ) ) )