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

Proof

Step	Hyp	Ref	Expression
1		iftrue	⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 )
2	1	con3i	⊢ ( ¬ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 → ¬ 𝜑 )
3	2	iffalsed	⊢ ( ¬ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 )
4	3	orri	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 ∨ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 )