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 ( -. ph , A , B ) = if ( ph , B , A )

Proof

Step	Hyp	Ref	Expression
1		notnot	|- ( ph -> -. -. ph )
2	1	iffalsed	|- ( ph -> if ( -. ph , A , B ) = B )
3		iftrue	|- ( ph -> if ( ph , B , A ) = B )
4	2 3	eqtr4d	|- ( ph -> if ( -. ph , A , B ) = if ( ph , B , A ) )
5		iftrue	|- ( -. ph -> if ( -. ph , A , B ) = A )
6		iffalse	|- ( -. ph -> if ( ph , B , A ) = A )
7	5 6	eqtr4d	|- ( -. ph -> if ( -. ph , A , B ) = if ( ph , B , A ) )
8	4 7	pm2.61i	|- if ( -. ph , A , B ) = if ( ph , B , A )