MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iffalse Unicode version

Theorem iffalse 3572
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.
StepHypRef Expression
1 dedlemb 921 . . 3  |-  ( -. 
ph  ->  ( x  e.  B  <->  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) ) )
21abbi2dv 2398 . 2  |-  ( -. 
ph  ->  B  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) } )
3 df-if 3566 . 2  |-  if (
ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
42, 3syl6reqr 2334 1  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357    /\ wa 358    = wceq 1623    e. wcel 1684   {cab 2269   ifcif 3565
This theorem is referenced by:  ifnefalse  3573  ifsb  3574  ifbi  3582  ifeq1da  3590  ifclda  3592  elimif  3594  ifbothda  3595  ifid  3597  ifeqor  3602  ifnot  3603  ifan  3604  ifor  3605  elimhyp  3613  elimhyp2v  3614  elimhyp3v  3615  elimhyp4v  3616  elimdhyp  3618  keephyp2v  3620  keephyp3v  3621  dfopif  3793  opprc  3817  somin1  5079  somincom  5080  dfiota4  5247  elimdelov  5927  riotav  6309  riotaund  6341  tz7.44-2  6420  tz7.44-3  6421  oevn0  6514  pw2f1olem  6966  unxpdomlem2  7068  unxpdomlem3  7069  oi0  7243  wemaplem2  7262  unwdomg  7298  ixpiunwdom  7305  cantnfp1lem1  7380  cantnfp1lem3  7382  cantnflem1d  7390  cantnflem1  7391  dfac12lem2  7770  fin23lem14  7959  axcc2lem  8062  ttukeylem5  8140  ttukeylem7  8142  canthp1lem2  8275  pwfseqlem3  8282  uzin  10260  xrmax1  10504  xrmax2  10505  xrmin1  10506  xrmin2  10507  max1ALT  10515  ifle  10524  xmulneg1  10589  rexmul  10591  xmulpnf1  10594  fzprval  10844  seqf1olem1  11085  seqf1olem2  11086  expnnval  11107  expneg  11111  bcval3  11319  ccatval2  11432  ccatco  11490  absmax  11813  sumeq2ii  12166  sumrblem  12184  fsumcvg  12185  summolem2a  12188  zsum  12191  sum0  12194  sumss  12197  sumss2  12199  fsumcvg2  12200  fsumsplit  12212  sumsplit  12231  ef0lem  12360  rpnnen2lem9  12501  ruclem2  12510  ruclem3  12511  sadadd2lem2  12641  sadcp1  12646  sadcaddlem  12648  sadadd2  12651  gcdn0val  12689  eucalgf  12753  eucalginv  12754  eucalglt  12755  iserodd  12888  pcgcd  12930  pcmptcl  12939  pcmpt  12940  pcmpt2  12941  pcprod  12943  fldivp1  12945  prmreclem2  12964  prmreclem4  12966  vdwlem6  13033  ramtub  13059  ressval2  13197  xpsaddlem  13477  xpsvsca  13481  setcepi  13920  gsumval2a  14459  mulgnn  14573  mulgnegnn  14577  odlem2  14854  dfod2  14877  gsumval3a  15189  gsumzsplit  15206  dmdprdsplitlem  15272  abvtrivd  15605  psrlidm  16148  psrridm  16149  mvridlem  16164  mvrf1  16170  mvrcl  16193  mplmon  16207  mplmonmul  16208  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  mplmon2  16234  psrbagsn  16236  coe1tmfv2  16351  obselocv  16628  ptpjpre1  17266  ptpjpre2  17275  ptbasfi  17276  ptopn2  17279  xkopt  17349  isfcls  17704  ptcmplem2  17747  ptcmplem3  17748  tsmssplit  17834  dscmet  18095  dscopn  18096  xrsxmet  18315  icccmplem2  18328  cnmpt2pc  18426  iccpnfcnv  18442  xrhmeo  18444  htpycc  18478  pco1  18513  pcoval2  18514  pcohtpylem  18517  pcopt  18520  pcopt2  18521  pcoass  18522  pcorevlem  18524  ovolunlem1a  18855  ovolunlem1  18856  ovolicc1  18875  i1f1lem  19044  itg11  19046  itg1addlem2  19052  itg1addlem3  19053  i1fres  19060  itg1climres  19069  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1flim  19078  itg2const2  19096  itg2seq  19097  itg2uba  19098  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  itgeq2  19132  itg0  19134  iblss  19159  iblss2  19160  itgle  19164  itgss  19166  itgss2  19167  itgss3  19169  itgless  19171  ibladdlem  19174  itgaddlem1  19177  iblabslem  19182  iblabs  19183  iblabsr  19184  iblmulc2  19185  bddmulibl  19193  itggt0  19196  itgcn  19197  ditgneg  19207  limccnp2  19242  dvexp2  19303  lhop2  19362  evlslem3  19398  evlslem1  19399  deg1add  19489  ig1pval3  19560  elply2  19578  ply1termlem  19585  plyeq0lem  19592  plypf1  19594  coeeq2  19624  dgrle  19625  coe1termlem  19639  dvply1  19664  vieta1lem2  19691  pserdvlem2  19804  abelthlem9  19816  logcnlem3  19991  logtayllem  20006  logtayl  20007  cxpef  20012  rlimcnp2  20261  efrlim  20264  isppw  20352  isnsqf  20373  mule1  20386  sqff1o  20420  muinv  20433  chtublem  20450  dchrelbasd  20478  bposlem1  20523  bposlem3  20525  bposlem5  20527  bposlem6  20528  lgsval2lem  20545  lgsval4  20555  lgsval4a  20557  lgsneg  20558  lgsneg1  20559  lgsdilem  20561  lgsdir2  20567  lgsdir  20569  lgsdi  20571  lgsne0  20572  rplogsumlem2  20634  dchrvmasum2if  20646  dchrisum0fno1  20660  rplogsum  20676  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  padicabv  20779  ostth1  20782  ostth2lem4  20785  ostth3  20787  gxpval  20926  gxnval  20927  ballotlemrv2  23080  ifbieq12d2  23149  elimifd  23151  elim2if  23152  partfun  23240  xrge0iifcnv  23315  xrge0iifcv  23316  xrge0iif1  23320  esumpinfval  23441  sigaclfu2  23482  itgmcntTMP  23588  indval2  23598  ind0  23603  dfrdg2  24152  dfrdg3  24153  unisnif  24464  dfrdg4  24488  axlowdimlem15  24584  axlowdim  24589  areacirclem6  24930  areacirc  24931  repcpwti  25161  dffprod  25319  isconc2  26007  lineval3a  26083  sgplpte22  26138  isray2  26153  fdc  26455  heiborlem4  26538  heiborlem6  26540  pw2f1ocnv  27130  aomclem5  27155  kelac1  27161  uvcvv0  27239  uvcff  27240  flcidc  27379  pmtrmvd  27398  mamulid  27458  mamurid  27459  refsum2cnlem1  27708  afvnfundmuv  28002  ifnmfalse  28233  sgnp  28247  sgnn  28251  cdleme27a  30556  cdleme31sn2  30578  cdleme31fv2  30582  cdlemefr27cl  30592  dihvalc  31423  mapdhval2  31916  hdmap1val2  31991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-if 3566
  Copyright terms: Public domain W3C validator