Theorem ifbieq2d

Description: Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011)

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

Proof

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