Theorem ifnot

Description: Negating the first argument swaps the last two arguments of a conditional operator. (Contributed by NM, 21-Jun-2007)

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

Proof

Step	Hyp	Ref	Expression
1		notnot	$$⊢\phi \to \neg \neg \phi$$
2	1	iffalsed	$$⊢\phi \to if\left(\neg \phi ,A,B\right)=B$$
3		iftrue	$$⊢\phi \to if\left(\phi ,B,A\right)=B$$
4	2 3	eqtr4d	$$⊢\phi \to if\left(\neg \phi ,A,B\right)=if\left(\phi ,B,A\right)$$
5		iftrue	$$⊢\neg \phi \to if\left(\neg \phi ,A,B\right)=A$$
6		iffalse	$$⊢\neg \phi \to if\left(\phi ,B,A\right)=A$$
7	5 6	eqtr4d	$$⊢\neg \phi \to if\left(\neg \phi ,A,B\right)=if\left(\phi ,B,A\right)$$
8	4 7	pm2.61i	$$⊢if\left(\neg \phi ,A,B\right)=if\left(\phi ,B,A\right)$$