Theorem iffalse

Description: Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999)

	Ref	Expression
Assertion	iffalse	|- ( -. ph -> if ( ph , A , B ) = B )

Proof

Step	Hyp	Ref	Expression
1		df-if	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
2		dedlemb	|- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
3	2	eqabdv	|- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
4	1 3	eqtr4id	|- ( -. ph -> if ( ph , A , B ) = B )