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

Theorem iffalse 3606
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 2431 . 2  |-  ( -. 
ph  ->  B  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) } )
3 df-if 3600 . 2  |-  if (
ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
42, 3syl6reqr 2367 1  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357    /\ wa 358    = wceq 1633    e. wcel 1701   {cab 2302   ifcif 3599
This theorem is referenced by:  ifnefalse  3607  ifsb  3608  ifbi  3616  ifeq1da  3624  ifclda  3626  elimif  3628  ifbothda  3629  ifid  3631  ifeqor  3636  ifnot  3637  ifan  3638  ifor  3639  elimhyp  3647  elimhyp2v  3648  elimhyp3v  3649  elimhyp4v  3650  elimdhyp  3652  keephyp2v  3654  keephyp3v  3655  dfopif  3830  opprc  3854  somin1  5116  somincom  5117  dfiota4  5284  elimdelov  5969  riotav  6351  riotaund  6383  tz7.44-2  6462  tz7.44-3  6463  oevn0  6556  pw2f1olem  7009  unxpdomlem2  7111  unxpdomlem3  7112  oi0  7288  wemaplem2  7307  unwdomg  7343  ixpiunwdom  7350  cantnfp1lem1  7425  cantnfp1lem3  7427  cantnflem1d  7435  cantnflem1  7436  dfac12lem2  7815  fin23lem14  8004  axcc2lem  8107  ttukeylem5  8185  ttukeylem7  8187  canthp1lem2  8320  pwfseqlem3  8327  uzin  10307  xrmax1  10551  xrmax2  10552  xrmin1  10553  xrmin2  10554  max1ALT  10562  ifle  10571  xmulneg1  10636  rexmul  10638  xmulpnf1  10641  fzprval  10891  seqf1olem1  11132  seqf1olem2  11133  expnnval  11154  expneg  11158  bcval3  11366  ccatval2  11479  ccatco  11537  absmax  11860  sumeq2ii  12213  sumrblem  12231  fsumcvg  12232  summolem2a  12235  zsum  12238  sum0  12241  sumss  12244  sumss2  12246  fsumcvg2  12247  fsumsplit  12259  sumsplit  12278  ef0lem  12407  rpnnen2lem9  12548  ruclem2  12557  ruclem3  12558  sadadd2lem2  12688  sadcp1  12693  sadcaddlem  12695  sadadd2  12698  gcdn0val  12736  eucalgf  12800  eucalginv  12801  eucalglt  12802  iserodd  12935  pcgcd  12977  pcmptcl  12986  pcmpt  12987  pcmpt2  12988  pcprod  12990  fldivp1  12992  prmreclem2  13011  prmreclem4  13013  vdwlem6  13080  ramtub  13106  ressval2  13244  xpsaddlem  13526  xpsvsca  13530  setcepi  13969  gsumval2a  14508  mulgnn  14622  mulgnegnn  14626  odlem2  14903  dfod2  14926  gsumval3a  15238  gsumzsplit  15255  dmdprdsplitlem  15321  abvtrivd  15654  psrlidm  16197  psrridm  16198  mvridlem  16213  mvrf1  16219  mvrcl  16242  mplmon  16256  mplmonmul  16257  mplcoe1  16258  mplcoe3  16259  mplcoe2  16260  mplmon2  16283  psrbagsn  16285  coe1tmfv2  16400  obselocv  16684  ptpjpre1  17322  ptpjpre2  17331  ptbasfi  17332  ptopn2  17335  xkopt  17405  isfcls  17756  ptcmplem2  17799  ptcmplem3  17800  tsmssplit  17886  dscmet  18147  dscopn  18148  xrsxmet  18367  icccmplem2  18380  cnmpt2pc  18479  iccpnfcnv  18495  xrhmeo  18497  htpycc  18531  pco1  18566  pcoval2  18567  pcohtpylem  18570  pcopt  18573  pcopt2  18574  pcoass  18575  pcorevlem  18577  ovolunlem1a  18908  ovolunlem1  18909  ovolicc1  18928  i1f1lem  19097  itg11  19099  itg1addlem2  19105  itg1addlem3  19106  i1fres  19113  itg1climres  19122  mbfi1fseqlem4  19126  mbfi1fseqlem5  19127  mbfi1flim  19131  itg2const2  19149  itg2seq  19150  itg2uba  19151  itg2splitlem  19156  itg2split  19157  itg2monolem1  19158  itg2gt0  19168  itg2cnlem1  19169  itg2cnlem2  19170  itgeq2  19185  itg0  19187  iblss  19212  iblss2  19213  itgle  19217  itgss  19219  itgss2  19220  itgss3  19222  itgless  19224  ibladdlem  19227  itgaddlem1  19230  iblabslem  19235  iblabs  19236  iblabsr  19237  iblmulc2  19238  bddmulibl  19246  itggt0  19249  itgcn  19250  ditgneg  19260  limccnp2  19295  dvexp2  19356  lhop2  19415  evlslem3  19451  evlslem1  19452  deg1add  19542  ig1pval3  19613  elply2  19631  ply1termlem  19638  plyeq0lem  19645  plypf1  19647  coeeq2  19677  dgrle  19678  coe1termlem  19692  dvply1  19717  vieta1lem2  19744  pserdvlem2  19857  abelthlem9  19869  logcnlem3  20044  logtayllem  20059  logtayl  20060  cxpef  20065  rlimcnp2  20314  efrlim  20317  isppw  20405  isnsqf  20426  mule1  20439  sqff1o  20473  muinv  20486  chtublem  20503  dchrelbasd  20531  bposlem1  20576  bposlem3  20578  bposlem5  20580  bposlem6  20581  lgsval2lem  20598  lgsval4  20608  lgsval4a  20610  lgsneg  20611  lgsneg1  20612  lgsdilem  20614  lgsdir2  20620  lgsdir  20622  lgsdi  20624  lgsne0  20625  rplogsumlem2  20687  dchrvmasum2if  20699  dchrisum0fno1  20713  rplogsum  20729  pntrlog2bndlem4  20782  pntrlog2bndlem5  20783  padicabv  20832  ostth1  20835  ostth2lem4  20838  ostth3  20840  gxpval  20979  gxnval  20980  ifbieq12d2  23145  elimifd  23147  elim2if  23148  xpima2  23186  imadifxp  23187  partfun  23237  xrge0iifcnv  23388  xrge0iifcv  23389  xrge0iif1  23393  esumpinfval  23639  sigaclfu2  23680  indval2  23827  ind0  23832  ballotlemrv2  23953  prodeq2ii  24416  prodrblem  24432  fprodcvg  24433  prodmolem2a  24437  zprod  24440  fprodntriv  24445  prod0  24446  prodss  24450  fprodsplit  24465  dfrdg2  24537  dfrdg3  24538  unisnif  24849  dfrdg4  24874  axlowdimlem15  24970  axlowdim  24975  itg2addnclem  25317  itg2addnclem2  25318  itg2addnc  25319  itg2gt0cn  25320  ibladdnclem  25321  itgaddnclem1  25323  itgaddnclem2  25324  iblabsnclem  25328  iblabsnc  25329  iblmulc2nc  25330  bddiblnc  25335  areacirclem6  25347  areacirc  25348  fdc  25604  heiborlem4  25686  heiborlem6  25688  pw2f1ocnv  26278  aomclem5  26303  kelac1  26309  uvcvv0  26387  uvcff  26388  flcidc  26527  pmtrmvd  26546  mamulid  26606  mamurid  26607  refsum2cnlem1  26856  afvnfundmuv  27152  ifnmfalse  27682  sgnp  27696  sgnn  27700  cdleme27a  30374  cdleme31sn2  30396  cdleme31fv2  30400  cdlemefr27cl  30410  dihvalc  31241  mapdhval2  31734  hdmap1val2  31809
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-if 3600
  Copyright terms: Public domain W3C validator