Theorem ifbieq2d

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

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

Proof

Step	Hyp	Ref	Expression
1		ifbieq2d.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
2		ifbieq2d.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3	1	ifbid	⊢ ( 𝜑 → if ( 𝜓 , 𝐶 , 𝐴 ) = if ( 𝜒 , 𝐶 , 𝐴 ) )
4	2	ifeq2d	⊢ ( 𝜑 → if ( 𝜒 , 𝐶 , 𝐴 ) = if ( 𝜒 , 𝐶 , 𝐵 ) )
5	3 4	eqtrd	⊢ ( 𝜑 → if ( 𝜓 , 𝐶 , 𝐴 ) = if ( 𝜒 , 𝐶 , 𝐵 ) )