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

Theorem iftrue 3573
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 )
Dummy variable  x is distinct from all other variables.

Proof of Theorem iftrue
StepHypRef Expression
1 dedlem0a 920 . . 3  |-  ( ph  ->  ( x  e.  A  <->  ( ( x  e.  B  ->  ph )  ->  (
x  e.  A  /\  ph ) ) ) )
21abbi2dv 2400 . 2  |-  ( ph  ->  A  =  { x  |  ( ( x  e.  B  ->  ph )  ->  ( x  e.  A  /\  ph ) ) } )
3 dfif2 3569 . 2  |-  if (
ph ,  A ,  B )  =  {
x  |  ( ( x  e.  B  ->  ph )  ->  ( x  e.  A  /\  ph ) ) }
42, 3syl6reqr 2336 1  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1624    e. wcel 1685   {cab 2271   ifcif 3567
This theorem is referenced by:  ifsb  3576  ifbi  3584  ifeq2da  3593  ifclda  3594  elimif  3596  ifbothda  3597  ifid  3599  ifeqor  3604  ifnot  3605  ifan  3606  ifor  3607  dedth  3608  elimhyp  3615  elimhyp2v  3616  elimhyp3v  3617  elimhyp4v  3618  elimdhyp  3620  keephyp2v  3622  keephyp3v  3623  dfopif  3795  dfopg  3796  somin1  5079  somincom  5080  elimdelov  5889  riotav  6305  riotaiota  6306  tz7.44-1  6415  tz7.44-3  6417  oe0m  6513  resixpfo  6850  boxriin  6854  boxcutc  6855  pw2f1olem  6962  unxpdomlem2  7064  unxpdomlem3  7065  ordtypelem1  7229  wemaplem2  7258  unwdomg  7294  ixpiunwdom  7301  cantnfp1lem2  7377  cantnfp1lem3  7378  acndom  7674  iunfictbso  7737  dfac12lem2  7766  fin23lem14  7955  axcc2lem  8058  ttukeylem4  8135  ttukeylem7  8138  pwfseqlem2  8277  uzin  10256  xrmax1  10499  xrmax2  10500  xrmin1  10501  xrmin2  10502  max1ALT  10510  max0sub  10518  ifle  10519  xnegpnf  10531  xnegmnf  10532  xaddpnf1  10548  xaddpnf2  10549  xaddmnf1  10550  xaddmnf2  10551  pnfaddmnf  10552  mnfaddpnf  10553  xmul01  10582  xmulneg1  10584  xmulpnf1  10589  fzprval  10839  fztpval  10840  seqf1olem1  11080  seqf1olem2  11081  expnnval  11102  exp0  11103  bcval2  11313  ccatval1  11426  swrd00  11446  swrdval2  11448  ccatco  11485  max0add  11790  absmax  11808  sumrblem  12179  fsumcvg  12180  summolem2a  12183  zsum  12186  isum  12187  sumss  12192  sumss2  12194  fsumcvg2  12195  fsumser  12198  fsumsplit  12207  sumsplit  12226  ef0lem  12355  rpnnen2lem3  12490  rpnnen2lem9  12496  ruclem2  12505  ruclem3  12506  sadadd2lem2  12636  sadcf  12639  sadc0  12640  sadcp1  12641  sadcaddlem  12643  smupf  12664  smup0  12665  gcd0val  12683  eucalgf  12748  eucalginv  12749  eucalglt  12750  iserodd  12883  pc0  12902  pcgcd  12925  pcmptcl  12934  pcmpt  12935  pcmpt2  12936  pcprod  12938  fldivp1  12940  prmreclem2  12959  prmreclem4  12961  1arithlem4  12968  vdwlem6  13028  ramtcl2  13053  ramcl2  13058  ramub1lem1  13068  ressid2  13191  xpscfv  13459  xpsfrnel  13460  xpsaddlem  13472  xpsvsca  13476  setcepi  13915  gsumval1  14451  gsumval2a  14454  mulg0  14567  mulgnn  14568  dfod2  14872  oddvds2  14874  frgpuptinv  15075  frgpup2  15080  frgpup3lem  15081  cyggenod  15166  cyggex  15179  gsumzsplit  15201  dprdfid  15247  dmdprdsplitlem  15267  abvtrivd  15600  psrlidm  16143  psrridm  16144  mvrid  16163  mvrf1  16165  mplmonmul  16203  mplcoe1  16204  mplcoe3  16205  mplcoe2  16206  mplmon2  16229  subrgasclcl  16235  coe1tm  16344  coe1tmfv1  16345  coe1tmmul2fv  16349  coe1pwmulfv  16351  coe1sclmul  16353  coe1sclmul2  16355  ply1sclid  16358  znf1o  16500  zzngim  16501  obsipid  16617  2ndcdisj  17177  ptpjpre1  17261  ptbasfi  17271  ptpjopn  17301  isfcls  17699  fclscmpi  17719  ptcmplem2  17742  ptcmplem3  17743  tsmssplit  17829  dscmet  18090  dscopn  18091  xrsxmet  18310  icccmplem2  18323  cnmpt2pc  18421  iccpnfcnv  18437  xrhmeo  18439  oprpiece1res1  18444  htpycc  18473  pcoval1  18506  pcohtpylem  18512  pcopt  18515  pcopt2  18516  pcoass  18517  pcorevlem  18519  cmetcaulem  18709  ovolunlem1a  18850  ovolunlem1  18851  ovolicc1  18870  ovolicc2lem3  18873  ovolicc2lem4  18874  ioorinv  18926  ioorcl  18927  i1f1lem  19039  itg11  19041  itg1addlem2  19047  itg1addlem4  19049  i1fres  19055  itg1climres  19064  mbfi1fseqlem4  19068  mbfi1fseqlem5  19069  mbfi1fseqlem6  19070  mbfi1flim  19073  itg2const2  19091  itg2seq  19092  itg2uba  19093  itg2splitlem  19098  itg2split  19099  itg2monolem1  19100  itg2cnlem1  19111  itg2cnlem2  19112  iblcnlem  19138  iblss  19154  iblss2  19155  itgitg2  19156  itgle  19159  itgss  19161  itgss2  19162  itgss3  19164  itgless  19166  ibladdlem  19169  itgaddlem1  19172  iblabslem  19177  iblabs  19178  iblabsr  19179  iblmulc2  19180  itgspliticc  19186  bddmulibl  19188  itggt0  19191  itgcn  19192  ditgpos  19201  limcvallem  19216  ellimc2  19222  limcres  19231  limccnp  19236  limccnp2  19237  limcco  19238  dvcobr  19290  dvexp2  19298  evlslem3  19393  evlslem1  19394  ig1pval2  19554  elply2  19573  elplyd  19579  ply1termlem  19580  plyeq0lem  19587  plypf1  19589  coeeq2  19619  coe1termlem  19634  dgrcolem2  19650  dvply1  19659  plydivlem4  19671  vieta1lem2  19686  aareccl  19701  dvtaylp  19744  pserdvlem2  19799  abelthlem9  19811  logtayl  20002  0cxp  20008  cxpexp  20010  leibpilem2  20232  leibpi  20233  rlimcnp2  20256  efrlim  20259  isppw  20347  vmappw  20349  muval1  20366  isnsqf  20368  mule1  20381  sqff1o  20415  muinv  20428  chtublem  20445  dchrelbasd  20473  dchr1  20491  dchrptlem2  20499  bposlem1  20518  bposlem3  20520  bposlem5  20522  bposlem6  20523  lgsval2lem  20540  lgs0  20543  lgs2  20547  lgsneg  20553  lgsdilem  20556  lgsdir2  20562  lgsdir  20564  lgsdi  20566  lgsne0  20567  rplogsumlem2  20629  dchrvmasum2if  20641  dchrvmasumiflem1  20645  dchrisum0flblem2  20653  dchrisum0fno1  20655  rpvmasum2  20656  rplogsum  20671  pntrlog2bndlem4  20724  pntrlog2bndlem5  20725  padicabv  20774  ostth2lem4  20780  gxpval  20919  gx0  20921  ballotlemsgt1  23063  ballotlemsel1i  23065  ballotlemsi  23067  ballotlemsima  23068  ballotlemrv1  23073  indispcon  23170  cvmliftlem10  23230  eupath2  23309  rdgprc0  23552  dfrdg2  23554  dfrdg3  23555  unisnif  23872  dfrdg4  23896  axlowdimlem15  23992  axlowdim  23997  repcpwti  24561  prod0  24705  isconc1  25406  isconc2  25407  lineval222  25479  sgplpte21  25532  isray  25554  fnejoin2  25718  sdclem1  25853  fdc  25855  heiborlem4  25938  pw2f1ocnv  26530  aomclem5  26555  kelac1  26561  uvcvv1  26638  flcidc  26779  pmtrprfv  26796  pmtrmvd  26798  pmtrfinv  26802  psgnunilem1  26816  mamulid  26858  mamurid  26859  sdrgacs  26909  phisum  26918  mon1pid  26924  refsum2cnlem1  27108  afvfundmfveq  27381  sgn0  27507  sgnn  27512  cdleme27a  29824  cdleme31sn1  29838  cdleme31fv1  29848  cdlemefs27cl  29870  cdlemk40t  30375  dihvalb  30695  mapdhval0  31183  hdmap1val0  31258
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-if 3568
  Copyright terms: Public domain W3C validator