Theorem iffalse 3579

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

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 710   = wceq 1373   e. wcel 2176   {cab 2191   ifcif 3571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-if 3572

This theorem is referenced by:  iffalsei  3580  iffalsed  3581  ifnefalse  3582  ifsbdc  3583  ifcldadc  3600  ifeq1dadc  3601  ifeqdadc  3603  ifbothdadc  3604  ifbothdc  3605  ifiddc  3606  ifcldcd  3608  ifnotdc  3609  ifandc  3610  ifordc  3611  ifnetruedc  3613  pw2f1odclem  6931  fidifsnen  6967  nnnninf  7228  uzin  9681  modifeq2int  10531  seqf1oglem1  10664  seqf1oglem2  10665  bcval  10894  bcval3  10896  sumrbdclem  11688  fsum3cvg  11689  summodclem2a  11692  sumsplitdc  11743  prodrbdclem  11882  fproddccvg  11883  prodssdc  11900  flodddiv4  12247  gcdn0val  12282  dfgcd2  12335  lcmn0val  12388  pcgcd  12652  pcmptcl  12665  pcmpt  12666  pcmpt2  12667  pcprod  12669  fldivp1  12671  unct  12813  lgsneg  15501  lgsdilem  15504  lgsdir2  15510  lgsdir  15512  lgsdi  15514  lgsne0  15515  gausslemma2dlem1a  15535  2lgslem1c  15567  2lgs  15581