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 ( ¬ 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜑 , 𝐵 , 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		notnot	⊢ ( 𝜑 → ¬ ¬ 𝜑 )
2	1	iffalsed	⊢ ( 𝜑 → if ( ¬ 𝜑 , 𝐴 , 𝐵 ) = 𝐵 )
3		iftrue	⊢ ( 𝜑 → if ( 𝜑 , 𝐵 , 𝐴 ) = 𝐵 )
4	2 3	eqtr4d	⊢ ( 𝜑 → if ( ¬ 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜑 , 𝐵 , 𝐴 ) )
5		iftrue	⊢ ( ¬ 𝜑 → if ( ¬ 𝜑 , 𝐴 , 𝐵 ) = 𝐴 )
6		iffalse	⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐵 , 𝐴 ) = 𝐴 )
7	5 6	eqtr4d	⊢ ( ¬ 𝜑 → if ( ¬ 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜑 , 𝐵 , 𝐴 ) )
8	4 7	pm2.61i	⊢ if ( ¬ 𝜑 , 𝐴 , 𝐵 ) = if ( 𝜑 , 𝐵 , 𝐴 )