Theorem ifbieq12i

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

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

Proof

Step	Hyp	Ref	Expression
1		ifbieq12i.1	$$⊢\phi \leftrightarrow \psi$$
2		ifbieq12i.2	$$⊢A=C$$
3		ifbieq12i.3	$$⊢B=D$$
4		ifeq1	$$⊢A=C\to if\left(\phi ,A,B\right)=if\left(\phi ,C,B\right)$$
5	2 4	ax-mp	$$⊢if\left(\phi ,A,B\right)=if\left(\phi ,C,B\right)$$
6	1 3	ifbieq2i	$$⊢if\left(\phi ,C,B\right)=if\left(\psi ,C,D\right)$$
7	5 6	eqtri	$$⊢if\left(\phi ,A,B\right)=if\left(\psi ,C,D\right)$$