Theorem iffalse 3924

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

Syntax hints:   -. wn 3   -> wi 4   \/ wo 369   /\ wa 370   = wceq 1437   e. wcel 1870   {cab 2414   ifcif 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-if 3916

This theorem is referenced by:  iffalsei  3925  iffalsed  3926  ifnefalse  3927  ifsb  3928  ifbi  3936  ifeq1da  3945  ifclda  3947  ifeqda  3948  elimif  3949  ifbothda  3950  ifid  3952  ifnot  3960  ifan  3961  ifor  3962  2if2  3963  ifcomnan  3964  elimhyp  3973  elimhyp2v  3974  elimhyp3v  3975  elimhyp4v  3976  elimdhyp  3978  keephyp2v  3980  keephyp3v  3981  dfopif  4187  opprc  4212  somin1  5253  dfiota4  5593  elimdelov  6386  ovif12  6389  oevn0  7225  pw2f1olem  7682  unxpdomlem2  7783  unxpdomlem3  7784  oi0  8043  wemaplem2  8062  ixpiunwdom  8106  cantnfp1lem3  8184  cantnflem1  8193  dfac12lem2  8572  fin23lem14  8761  axcc2lem  8864  ttukeylem5  8941  uzin  11191  xrmax1  11470  xrmax2  11471  xrmin1  11472  xrmin2  11473  max1ALT  11481  ifle  11490  xmulneg1  11555  modifeq2int  12149  seqf1olem1  12249  seqf1olem2  12250  bcval3  12488  swrdccat  12834  swrdccat3a  12835  swrdccat3b  12837  repswswrd  12872  cshword  12878  ccatco  12917  sumrblem  13755  fsumcvg  13756  summolem2a  13759  sumss  13768  fsumcvg2  13771  sumsplit  13807  prodeq2ii  13945  prodrblem  13961  fprodcvg  13962  prodmolem2a  13966  zprod  13969  prodss  13979  ruclem2  14262  ruclem3  14263  sadadd2lem2  14398  sadcp1  14403  sadcaddlem  14405  gcdn0val  14446  lcmn0val  14530  lcmn0valOLD  14531  lcmfn0val  14564  lcmfn0valOLD  14567  pcgcd  14790  pcmptcl  14799  pcmpt  14800  pcmpt2  14801  pcprod  14803  fldivp1  14805  prmreclem2  14824  prmreclem4  14826  vdwlem6  14899  prmo1  14958  prmop1  14959  fvprmselelfz  14965  fvprmselgcd1  14966  ressval2  15140  xpsaddlem  15432  xpsvsca  15436  setcepi  15934  pmtrmvd  17048  mvrf1  18584  mplcoe3  18625  mplmon2  18651  psrbagsn  18653  evlslem1  18673  obselocv  19222  dmatmul  19453  1mavmul  19504  mulmarep1gsum2  19530  1marepvmarrepid  19531  mdetdiag  19555  mdetrsca2  19560  mdetrlin2  19563  mdetunilem5  19572  mdetunilem7  19574  mdetunilem8  19575  mdetunilem9  19576  mndifsplit  19592  maducoeval2  19596  madugsum  19599  madurid  19600  smadiadetglem2  19628  1elcpmat  19670  decpmatid  19725  ptpjpre1  20517  ptbasfi  20527  isfcls  20955  ptcmplem2  20999  ptcmplem3  21000  dscmet  21518  dscopn  21519  icccmplem2  21752  cnmpt2pc  21852  iccpnfcnv  21868  xrhmeo  21870  pcoval2  21940  pcohtpylem  21943  pcopt  21946  pcopt2  21947  pcoass  21948  pcorevlem  21950  i1f1lem  22524  itg1addlem2  22532  itg1addlem3  22533  i1fres  22540  itg1climres  22549  mbfi1fseqlem4  22553  mbfi1fseqlem5  22554  itg2const2  22576  itg2seq  22577  itg2uba  22578  itg2splitlem  22583  itg2split  22584  itg2monolem1  22585  itg2gt0  22595  itg2cnlem1  22596  itg2cnlem2  22597  iblss  22639  iblss2  22640  itgle  22644  itgss  22646  ibladdlem  22654  itgaddlem1  22657  iblabslem  22662  iblabs  22663  iblabsr  22664  iblmulc2  22665  bddmulibl  22673  ditgneg  22689  elply2  23018  coeeq2  23064  dgrle  23065  coe1termlem  23080  logcnlem3  23454  igamgam  23839  isppw  23904  isnsqf  23925  mule1  23938  sqff1o  23972  chtublem  24002  dchrelbasd  24030  bposlem1  24075  bposlem3  24077  bposlem5  24079  bposlem6  24080  lgsneg  24110  lgsdilem  24113  lgsdir2  24119  lgsdir  24121  lgsdi  24123  lgsne0  24124  dchrvmasum2if  24198  ostth2lem4  24337  axlowdimlem15  24832  ifbieq12d2  27998  elimifd  27999  elim2if  28000  imadifxp  28051  resvval2  28431  xrge0iifcnv  28578  indval2  28675  ddeval0  28897  eulerpartlemb  29027  plymulx0  29224  signsw0glem  29230  signswmnd  29234  dfrdg2  30229  dfrdg3  30230  unisnif  30477  dfrdg4  30503  bj-xpima1sn  31298  poimirlem15  31659  poimirlem23  31667  mbfposadd  31692  itg2addnclem  31697  itg2addnclem3  31699  itg2gt0cn  31701  ibladdnclem  31702  itgaddnclem1  31704  iblabsnclem  31709  iblabsnc  31710  iblmulc2nc  31711  bddiblnc  31716  ftc1anclem5  31725  ftc1anclem7  31727  ftc1anclem8  31728  ftc1anc  31729  areacirclem5  31740  areacirc  31741  heiborlem4  31850  ac6s6  32119  riotaclbgBAD  32235  cdleme27a  33643  cdleme31sn2  33665  dihvalc  34510  mapdhval2  35003  hdmap1val2  35078  pw2f1ocnv  35598  aomclem5  35622  arearect  35799  areaquad  35800  upbdrech2  37135  lptioo2  37283  lptioo1  37284  coskpi2  37313  cosknegpi  37316  icccncfext  37337  cncfiooicclem1  37343  cncfiooiccre  37345  ioodvbdlimc1lem2  37376  ioodvbdlimc2lem  37378  itgioocnicc  37423  iblcncfioo  37424  dirkerper  37527  dirkertrigeq  37532  dirkercncflem2  37535  fourierdlem10  37548  fourierdlem32  37570  fourierdlem33  37571  fourierdlem37  37575  fourierdlem62  37600  fourierdlem73  37611  fourierdlem74  37612  fourierdlem75  37613  fourierdlem79  37617  fourierdlem81  37619  fourierdlem82  37620  fourierdlem93  37631  fourierdlem97  37635  fourierdlem101  37639  fourierdlem103  37641  fourierdlem104  37642  sqwvfoura  37660  sqwvfourb  37661  fourierswlem  37662  fouriersw  37663  elaa2lem  37665  etransclem15  37681  etransclem19  37685  etransclem23  37689  etransclem24  37690  etransclem25  37691  nnfoctbdjlem  37802  afvnfundmuv  38031  pfxccat3a  38360  cshword2  38368  suppmptcfin  38924  linc1  38978  ifnmfalse  39244