Theorem ifbieq12d

Description: Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypotheses	ifbieq12d.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
	ifbieq12d.2	$$⊢\phi \to A=C$$
	ifbieq12d.3	$$⊢\phi \to B=D$$
Assertion	ifbieq12d	$$⊢\phi \to if\left(\psi ,A,B\right)=if\left(\chi ,C,D\right)$$

Proof

Step	Hyp	Ref	Expression
1		ifbieq12d.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
2		ifbieq12d.2	$$⊢\phi \to A=C$$
3		ifbieq12d.3	$$⊢\phi \to B=D$$
4	1	ifbid	$$⊢\phi \to if\left(\psi ,A,B\right)=if\left(\chi ,A,B\right)$$
5	2 3	ifeq12d	$$⊢\phi \to if\left(\chi ,A,B\right)=if\left(\chi ,C,D\right)$$
6	4 5	eqtrd	$$⊢\phi \to if\left(\psi ,A,B\right)=if\left(\chi ,C,D\right)$$