Theorem ifbieq2i

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

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

Proof

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