Theorem ifbieq12i

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

	Ref	Expression
Hypotheses	ifbieq12i.1	⊢ ( 𝜑 ↔ 𝜓 )
	ifbieq12i.2	⊢ 𝐴 = 𝐶
	ifbieq12i.3	⊢ 𝐵 = 𝐷
Assertion	ifbieq12i	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐶 , 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		ifbieq12i.1	⊢ ( 𝜑 ↔ 𝜓 )
2		ifbieq12i.2	⊢ 𝐴 = 𝐶
3		ifbieq12i.3	⊢ 𝐵 = 𝐷
4		ifeq1	⊢ ( 𝐴 = 𝐶 → if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜑 , 𝐶 , 𝐵 ) )
5	2 4	ax-mp	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜑 , 𝐶 , 𝐵 )
6	1 3	ifbieq2i	⊢ if ( 𝜑 , 𝐶 , 𝐵 ) = if ( 𝜓 , 𝐶 , 𝐷 )
7	5 6	eqtri	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜓 , 𝐶 , 𝐷 )