Theorem ifeqor

Description: The possible values of a conditional operator. (Contributed by NM, 17-Jun-2007) (Proof shortened by Andrew Salmon, 26-Jun-2011)

	Ref	Expression
Assertion	ifeqor	$$⊢\left(if\left(\phi ,A,B\right)=A\vee if\left(\phi ,A,B\right)=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		iftrue	$$⊢\phi \to if\left(\phi ,A,B\right)=A$$
2	1	con3i	$$⊢\neg if\left(\phi ,A,B\right)=A\to \neg \phi$$
3	2	iffalsed	$$⊢\neg if\left(\phi ,A,B\right)=A\to if\left(\phi ,A,B\right)=B$$
4	3	orri	$$⊢\left(if\left(\phi ,A,B\right)=A\vee if\left(\phi ,A,B\right)=B\right)$$