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		dedlemb	|- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
2	1	abbi2dv	|- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
3		df-if	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
4	2 3	syl6reqr	|- ( -. ph -> if ( ph , A , B ) = B )