Theorem ifbi

Description: Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004)

	Ref	Expression
Assertion	ifbi	$$⊢\left(\phi \leftrightarrow \psi \right)\to if\left(\phi ,A,B\right)=if\left(\psi ,A,B\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfbi3	$$⊢\left(\phi \leftrightarrow \psi \right)\leftrightarrow \left(\left(\phi \wedge \psi \right)\vee \left(\neg \phi \wedge \neg \psi \right)\right)$$
2		iftrue	$$⊢\phi \to if\left(\phi ,A,B\right)=A$$
3		iftrue	$$⊢\psi \to if\left(\psi ,A,B\right)=A$$
4	3	eqcomd	$$⊢\psi \to A=if\left(\psi ,A,B\right)$$
5	2 4	sylan9eq	$$⊢\left(\phi \wedge \psi \right)\to if\left(\phi ,A,B\right)=if\left(\psi ,A,B\right)$$
6		iffalse	$$⊢\neg \phi \to if\left(\phi ,A,B\right)=B$$
7		iffalse	$$⊢\neg \psi \to if\left(\psi ,A,B\right)=B$$
8	7	eqcomd	$$⊢\neg \psi \to B=if\left(\psi ,A,B\right)$$
9	6 8	sylan9eq	$$⊢\left(\neg \phi \wedge \neg \psi \right)\to if\left(\phi ,A,B\right)=if\left(\psi ,A,B\right)$$
10	5 9	jaoi	$$⊢\left(\left(\phi \wedge \psi \right)\vee \left(\neg \phi \wedge \neg \psi \right)\right)\to if\left(\phi ,A,B\right)=if\left(\psi ,A,B\right)$$
11	1 10	sylbi	$$⊢\left(\phi \leftrightarrow \psi \right)\to if\left(\phi ,A,B\right)=if\left(\psi ,A,B\right)$$