Theorem iffalse 3381

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

Assertion

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

Proof of Theorem iffalse

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dedlemb 912	. . 3 |- ( -. ph -> ( x e. B <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) ) )
2	1	abbi2dv 2201	. 2 |- ( -. ph -> B = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } )
3		df-if 3374	. 2 |- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
4	2, 3	syl6reqr 2134	1 |- ( -. ph -> if ( ph , A , B ) = B )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 102   \/ wo 662   = wceq 1285   e. wcel 1434   {cab 2069   ifcif 3373

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-if 3374

This theorem is referenced by:  iffalsei  3382  iffalsed  3383  ifnefalse  3384  ifsbdc  3385  ifcldadc  3400  ifeq1dadc  3401  ifbothdadc  3402  ifbothdc  3403  ifcldcd  3405  fidifsnen  6516  nnnninf  8645  uzin  8946  modifeq2int  9682  expival  9794  bcval  9992  bcval3  9994  isumrblem  10573  fisumcvg  10574  flodddiv4  10714  gcdn0val  10733  dfgcd2  10783  lcmn0val  10828