Theorem ifbieq2i

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

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

Proof

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