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 ) ) )