Theorem ifbieq12i

Description: Equivalence deduction for conditional operators. (Contributed by NM, 18-Mar-2013)

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

Proof

Step	Hyp	Ref	Expression
1		ifbieq12i.1	|- ( ph <-> ps )
2		ifbieq12i.2	|- A = C
3		ifbieq12i.3	|- B = D
4		ifeq1	|- ( A = C -> if ( ph , A , B ) = if ( ph , C , B ) )
5	2 4	ax-mp	|- if ( ph , A , B ) = if ( ph , C , B )
6	1 3	ifbieq2i	|- if ( ph , C , B ) = if ( ps , C , D )
7	5 6	eqtri	|- if ( ph , A , B ) = if ( ps , C , D )