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

Theorem iftrue 3571
Description: Value of the conditional operator when its first argument is true. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
iftrue  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )

Proof of Theorem iftrue
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dedlem0a 918 . . 3  |-  ( ph  ->  ( x  e.  A  <->  ( ( x  e.  B  ->  ph )  ->  (
x  e.  A  /\  ph ) ) ) )
21abbi2dv 2398 . 2  |-  ( ph  ->  A  =  { x  |  ( ( x  e.  B  ->  ph )  ->  ( x  e.  A  /\  ph ) ) } )
3 dfif2 3567 . 2  |-  if (
ph ,  A ,  B )  =  {
x  |  ( ( x  e.  B  ->  ph )  ->  ( x  e.  A  /\  ph ) ) }
42, 3syl6reqr 2334 1  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684   {cab 2269   ifcif 3565
This theorem is referenced by:  ifsb  3574  ifbi  3582  ifeq2da  3591  ifclda  3592  elimif  3594  ifbothda  3595  ifid  3597  ifeqor  3602  ifnot  3603  ifan  3604  ifor  3605  dedth  3606  elimhyp  3613  elimhyp2v  3614  elimhyp3v  3615  elimhyp4v  3616  elimdhyp  3618  keephyp2v  3620  keephyp3v  3621  dfopif  3793  dfopg  3794  somin1  5079  somincom  5080  dfiota4  5247  elimdelov  5927  riotav  6309  riotaiota  6310  tz7.44-1  6419  tz7.44-3  6421  oe0m  6517  resixpfo  6854  boxriin  6858  boxcutc  6859  pw2f1olem  6966  unxpdomlem2  7068  unxpdomlem3  7069  ordtypelem1  7233  wemaplem2  7262  unwdomg  7298  ixpiunwdom  7305  cantnfp1lem2  7381  cantnfp1lem3  7382  acndom  7678  iunfictbso  7741  dfac12lem2  7770  fin23lem14  7959  axcc2lem  8062  ttukeylem4  8139  ttukeylem7  8142  pwfseqlem2  8281  uzin  10260  xrmax1  10504  xrmax2  10505  xrmin1  10506  xrmin2  10507  max1ALT  10515  max0sub  10523  ifle  10524  xnegpnf  10536  xnegmnf  10537  xaddpnf1  10553  xaddpnf2  10554  xaddmnf1  10555  xaddmnf2  10556  pnfaddmnf  10557  mnfaddpnf  10558  xmul01  10587  xmulneg1  10589  xmulpnf1  10594  fzprval  10844  fztpval  10845  seqf1olem1  11085  seqf1olem2  11086  expnnval  11107  exp0  11108  bcval2  11318  ccatval1  11431  swrd00  11451  swrdval2  11453  ccatco  11490  max0add  11795  absmax  11813  sumrblem  12184  fsumcvg  12185  summolem2a  12188  zsum  12191  isum  12192  sumss  12197  sumss2  12199  fsumcvg2  12200  fsumser  12203  fsumsplit  12212  sumsplit  12231  ef0lem  12360  rpnnen2lem3  12495  rpnnen2lem9  12501  ruclem2  12510  ruclem3  12511  sadadd2lem2  12641  sadcf  12644  sadc0  12645  sadcp1  12646  sadcaddlem  12648  smupf  12669  smup0  12670  gcd0val  12688  eucalgf  12753  eucalginv  12754  eucalglt  12755  iserodd  12888  pc0  12907  pcgcd  12930  pcmptcl  12939  pcmpt  12940  pcmpt2  12941  pcprod  12943  fldivp1  12945  prmreclem2  12964  prmreclem4  12966  1arithlem4  12973  vdwlem6  13033  ramtcl2  13058  ramcl2  13063  ramub1lem1  13073  ressid2  13196  xpscfv  13464  xpsfrnel  13465  xpsaddlem  13477  xpsvsca  13481  setcepi  13920  gsumval1  14456  gsumval2a  14459  mulg0  14572  mulgnn  14573  dfod2  14877  oddvds2  14879  frgpuptinv  15080  frgpup2  15085  frgpup3lem  15086  cyggenod  15171  cyggex  15184  gsumzsplit  15206  dprdfid  15252  dmdprdsplitlem  15272  abvtrivd  15605  psrlidm  16148  psrridm  16149  mvrid  16168  mvrf1  16170  mplmonmul  16208  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  mplmon2  16234  subrgasclcl  16240  coe1tm  16349  coe1tmfv1  16350  coe1tmmul2fv  16354  coe1pwmulfv  16356  coe1sclmul  16358  coe1sclmul2  16360  ply1sclid  16363  znf1o  16505  zzngim  16506  obsipid  16622  2ndcdisj  17182  ptpjpre1  17266  ptbasfi  17276  ptpjopn  17306  isfcls  17704  fclscmpi  17724  ptcmplem2  17747  ptcmplem3  17748  tsmssplit  17834  dscmet  18095  dscopn  18096  xrsxmet  18315  icccmplem2  18328  cnmpt2pc  18426  iccpnfcnv  18442  xrhmeo  18444  oprpiece1res1  18449  htpycc  18478  pcoval1  18511  pcohtpylem  18517  pcopt  18520  pcopt2  18521  pcoass  18522  pcorevlem  18524  cmetcaulem  18714  ovolunlem1a  18855  ovolunlem1  18856  ovolicc1  18875  ovolicc2lem3  18878  ovolicc2lem4  18879  ioorinv  18931  ioorcl  18932  i1f1lem  19044  itg11  19046  itg1addlem2  19052  itg1addlem4  19054  i1fres  19060  itg1climres  19069  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1fseqlem6  19075  mbfi1flim  19078  itg2const2  19096  itg2seq  19097  itg2uba  19098  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2cnlem1  19116  itg2cnlem2  19117  iblcnlem  19143  iblss  19159  iblss2  19160  itgitg2  19161  itgle  19164  itgss  19166  itgss2  19167  itgss3  19169  itgless  19171  ibladdlem  19174  itgaddlem1  19177  iblabslem  19182  iblabs  19183  iblabsr  19184  iblmulc2  19185  itgspliticc  19191  bddmulibl  19193  itggt0  19196  itgcn  19197  ditgpos  19206  limcvallem  19221  ellimc2  19227  limcres  19236  limccnp  19241  limccnp2  19242  limcco  19243  dvcobr  19295  dvexp2  19303  evlslem3  19398  evlslem1  19399  ig1pval2  19559  elply2  19578  elplyd  19584  ply1termlem  19585  plyeq0lem  19592  plypf1  19594  coeeq2  19624  coe1termlem  19639  dgrcolem2  19655  dvply1  19664  plydivlem4  19676  vieta1lem2  19691  aareccl  19706  dvtaylp  19749  pserdvlem2  19804  abelthlem9  19816  logtayl  20007  0cxp  20013  cxpexp  20015  leibpilem2  20237  leibpi  20238  rlimcnp2  20261  efrlim  20264  isppw  20352  vmappw  20354  muval1  20371  isnsqf  20373  mule1  20386  sqff1o  20420  muinv  20433  chtublem  20450  dchrelbasd  20478  dchr1  20496  dchrptlem2  20504  bposlem1  20523  bposlem3  20525  bposlem5  20527  bposlem6  20528  lgsval2lem  20545  lgs0  20548  lgs2  20552  lgsneg  20558  lgsdilem  20561  lgsdir2  20567  lgsdir  20569  lgsdi  20571  lgsne0  20572  rplogsumlem2  20634  dchrvmasum2if  20646  dchrvmasumiflem1  20650  dchrisum0flblem2  20658  dchrisum0fno1  20660  rpvmasum2  20661  rplogsum  20676  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  padicabv  20779  ostth2lem4  20785  gxpval  20926  gx0  20928  ballotlemsgt1  23069  ballotlemsel1i  23071  ballotlemsi  23073  ballotlemsima  23074  ballotlemrv1  23079  ifbieq12d2  23149  elimifd  23151  elim2if  23152  partfun  23240  xrge0iifcnv  23315  xrge0iifiso  23317  xrge0iifhom  23319  esumpinfval  23441  sigaclfu2  23482  itgmvolTMP  23587  itgmcntTMP  23588  indval2  23598  ind1  23602  indispcon  23765  cvmliftlem10  23825  eupath2  23904  rdgprc0  24150  dfrdg2  24152  dfrdg3  24153  unisnif  24464  dfrdg4  24488  axlowdimlem15  24584  axlowdim  24589  areacirclem6  24930  areacirc  24931  repcpwti  25161  prod0  25305  isconc1  26006  isconc2  26007  lineval222  26079  sgplpte21  26132  isray  26154  fnejoin2  26318  sdclem1  26453  fdc  26455  heiborlem4  26538  pw2f1ocnv  27130  aomclem5  27155  kelac1  27161  uvcvv1  27238  flcidc  27379  pmtrprfv  27396  pmtrmvd  27398  pmtrfinv  27402  psgnunilem1  27416  mamulid  27458  mamurid  27459  sdrgacs  27509  phisum  27518  mon1pid  27524  refsum2cnlem1  27708  afvfundmfveq  28001  sgn0  28246  sgnn  28251  cdleme27a  30556  cdleme31sn1  30570  cdleme31fv1  30580  cdlemefs27cl  30602  cdlemk40t  31107  dihvalb  31427  mapdhval0  31915  hdmap1val0  31990
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