Theorem iffalse 3950

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

Assertion

Ref	Expression
iffalse

Proof of Theorem iffalse

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dedlemb 955	. . 3
2	1	abbi2dv 2594	. 2
3		df-if 3942	. 2
4	2, 3	syl6reqr 2517	1

Syntax hints:  -.wn 3  ->wi 4  \/wo 368  /\wa 369  =wceq 1395  e.wcel 1818  {cab 2442  ifcif 3941

This theorem is referenced by:  iffalsei  3951  iffalsed  3952  ifnefalse  3953  ifsb  3954  ifbi  3962  ifeq1da  3971  ifclda  3973  ifeqda  3974  elimif  3975  ifbothda  3976  ifid  3978  ifnot  3986  ifan  3987  ifor  3988  2if2  3989  ifcomnan  3990  elimhyp  4000  elimhyp2v  4001  elimhyp3v  4002  elimhyp4v  4003  elimdhyp  4005  keephyp2v  4007  keephyp3v  4008  dfopif  4214  opprc  4239  somin1  5408  dfiota4  5584  elimdelov  6378  ovif12  6381  oevn0  7184  pw2f1olem  7641  unxpdomlem2  7745  unxpdomlem3  7746  oi0  7974  wemaplem2  7993  ixpiunwdom  8038  cantnfp1lem3  8120  cantnflem1  8129  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  cantnflem1dOLD  8151  cantnflem1OLD  8152  dfac12lem2  8545  fin23lem14  8734  axcc2lem  8837  ttukeylem5  8914  uzin  11142  xrmax1  11405  xrmax2  11406  xrmin1  11407  xrmin2  11408  max1ALT  11416  ifle  11425  xmulneg1  11490  modifeq2int  12049  seqf1olem1  12146  seqf1olem2  12147  bcval3  12384  swrdccat  12718  swrdccat3a  12719  swrdccat3b  12721  repswswrd  12756  cshword  12762  ccatco  12801  sumrblem  13533  fsumcvg  13534  summolem2a  13537  sumss  13546  fsumcvg2  13549  sumsplit  13583  prodeq2ii  13720  prodrblem  13736  fprodcvg  13737  prodmolem2a  13741  zprod  13744  prodss  13754  ruclem2  13965  ruclem3  13966  sadadd2lem2  14100  sadcp1  14105  sadcaddlem  14107  gcdn0val  14148  pcgcd  14401  pcmptcl  14410  pcmpt  14411  pcmpt2  14412  pcprod  14414  fldivp1  14416  prmreclem2  14435  prmreclem4  14437  vdwlem6  14504  ressval2  14686  xpsaddlem  14972  xpsvsca  14976  setcepi  15415  pmtrmvd  16481  gsumval3aOLD  16906  gsumzsplitOLD  16945  dmdprdsplitlemOLD  17085  psrlidmOLD  18057  psrridmOLD  18059  mvridlemOLD  18075  mvrf1  18081  mplcoe3  18128  mplcoe3OLD  18129  mplcoe2OLD  18133  mplmon2  18158  psrbagsn  18160  evlslem1  18184  obselocv  18759  dmatmul  18999  1mavmul  19050  mulmarep1gsum2  19076  1marepvmarrepid  19077  mdetdiag  19101  mdetrsca2  19106  mdetrlin2  19109  mdetunilem5  19118  mdetunilem7  19120  mdetunilem8  19121  mdetunilem9  19122  mndifsplit  19138  maducoeval2  19142  madugsum  19145  madurid  19146  smadiadetglem2  19174  1elcpmat  19216  decpmatid  19271  ptpjpre1  20072  ptbasfi  20082  isfcls  20510  ptcmplem2  20553  ptcmplem3  20554  dscmet  21093  dscopn  21094  icccmplem2  21328  cnmpt2pc  21428  iccpnfcnv  21444  xrhmeo  21446  pcoval2  21516  pcohtpylem  21519  pcopt  21522  pcopt2  21523  pcoass  21524  pcorevlem  21526  i1f1lem  22096  itg1addlem2  22104  itg1addlem3  22105  i1fres  22112  itg1climres  22121  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  itg2const2  22148  itg2seq  22149  itg2uba  22150  itg2splitlem  22155  itg2split  22156  itg2monolem1  22157  itg2gt0  22167  itg2cnlem1  22168  itg2cnlem2  22169  iblss  22211  iblss2  22212  itgle  22216  itgss  22218  ibladdlem  22226  itgaddlem1  22229  iblabslem  22234  iblabs  22235  iblabsr  22236  iblmulc2  22237  bddmulibl  22245  ditgneg  22261  elply2  22593  coeeq2  22639  dgrle  22640  coe1termlem  22655  logcnlem3  23025  isppw  23388  isnsqf  23409  mule1  23422  sqff1o  23456  chtublem  23486  dchrelbasd  23514  bposlem1  23559  bposlem3  23561  bposlem5  23563  bposlem6  23564  lgsneg  23594  lgsdilem  23597  lgsdir2  23603  lgsdir  23605  lgsdi  23607  lgsne0  23608  dchrvmasum2if  23682  ostth2lem4  23821  axlowdimlem15  24259  ifbieq12d2  27420  elimifd  27421  elim2if  27422  imadifxp  27458  resvval2  27819  xrge0iifcnv  27915  indval2  28028  ddeval0  28207  eulerpartlemb  28307  plymulx0  28504  signsw0glem  28510  signswmnd  28514  igamgam  28591  dfrdg2  29228  dfrdg3  29229  unisnif  29575  dfrdg4  29600  mbfposadd  30062  itg2addnclem  30066  itg2addnclem3  30068  itg2gt0cn  30070  ibladdnclem  30071  itgaddnclem1  30073  iblabsnclem  30078  iblabsnc  30079  iblmulc2nc  30080  bddiblnc  30085  ftc1anclem5  30094  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  areacirclem5  30111  areacirc  30112  heiborlem4  30310  ac6s6  30580  pw2f1ocnv  30979  aomclem5  31004  arearect  31183  areaquad  31184  lcmn0val  31201  upbdrech2  31508  lptioo2  31637  lptioo1  31638  coskpi2  31666  cosknegpi  31669  icccncfext  31690  cncfiooicclem1  31696  cncfiooiccre  31698  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  itgioocnicc  31776  iblcncfioo  31777  dirkerper  31878  dirkertrigeq  31883  dirkercncflem2  31886  fourierdlem10  31899  fourierdlem32  31921  fourierdlem33  31922  fourierdlem37  31926  fourierdlem62  31951  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem79  31968  fourierdlem81  31970  fourierdlem82  31971  fourierdlem93  31982  fourierdlem97  31986  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  elaa2lem  32016  etransclem15  32032  etransclem19  32036  etransclem23  32040  etransclem24  32041  etransclem25  32042  afvnfundmuv  32224  suppmptcfin  32972  linc1  33026  ifnmfalse  33157  bj-xpima1sn  34513  riotaclbgBAD  34685  cdleme27a  36093  cdleme31sn2  36115  dihvalc  36960  mapdhval2  37453  hdmap1val2  37528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-if 3942