Theorem ifbieq12d

Description: Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypotheses	ifbieq12d.1	|- ( ph -> ( ps <-> ch ) )
	ifbieq12d.2	|- ( ph -> A = C )
	ifbieq12d.3	|- ( ph -> B = D )
Assertion	ifbieq12d	|- ( ph -> if ( ps , A , B ) = if ( ch , C , D ) )

Proof

Step	Hyp	Ref	Expression
1		ifbieq12d.1	|- ( ph -> ( ps <-> ch ) )
2		ifbieq12d.2	|- ( ph -> A = C )
3		ifbieq12d.3	|- ( ph -> B = D )
4	1	ifbid	|- ( ph -> if ( ps , A , B ) = if ( ch , A , B ) )
5	2 3	ifeq12d	|- ( ph -> if ( ch , A , B ) = if ( ch , C , D ) )
6	4 5	eqtrd	|- ( ph -> if ( ps , A , B ) = if ( ch , C , D ) )