Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 iftrue 
 |-  ( ph -> if ( ph , A , B ) = A )
2 1 con3i 
 |-  ( -. if ( ph , A , B ) = A -> -. ph )
3 2 iffalsed 
 |-  ( -. if ( ph , A , B ) = A -> if ( ph , A , B ) = B )
4 3 orri 
 |-  ( if ( ph , A , B ) = A \/ if ( ph , A , B ) = B )