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

Theorem iftrue 3737
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 919 . . 3  |-  ( ph  ->  ( x  e.  A  <->  ( ( x  e.  B  ->  ph )  ->  (
x  e.  A  /\  ph ) ) ) )
21abbi2dv 2550 . 2  |-  ( ph  ->  A  =  { x  |  ( ( x  e.  B  ->  ph )  ->  ( x  e.  A  /\  ph ) ) } )
3 dfif2 3733 . 2  |-  if (
ph ,  A ,  B )  =  {
x  |  ( ( x  e.  B  ->  ph )  ->  ( x  e.  A  /\  ph ) ) }
42, 3syl6reqr 2486 1  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    e. wcel 1725   {cab 2421   ifcif 3731
This theorem is referenced by:  ifsb  3740  ifbi  3748  ifeq2da  3757  ifclda  3758  elimif  3760  ifbothda  3761  ifid  3763  ifeqor  3768  ifnot  3769  ifan  3770  ifor  3771  dedth  3772  elimhyp  3779  elimhyp2v  3780  elimhyp3v  3781  elimhyp4v  3782  elimdhyp  3784  keephyp2v  3786  keephyp3v  3787  dfopif  3973  dfopg  3974  somin1  5261  somincom  5262  xpima1  5305  dfiota4  5437  elimdelov  6144  riotav  6545  riotaiota  6546  tz7.44-1  6655  tz7.44-3  6657  oe0m  6753  resixpfo  7091  boxriin  7095  boxcutc  7096  pw2f1olem  7203  unxpdomlem2  7305  unxpdomlem3  7306  ordtypelem1  7476  wemaplem2  7505  unwdomg  7541  ixpiunwdom  7548  cantnfp1lem2  7624  cantnfp1lem3  7625  acndom  7921  iunfictbso  7984  dfac12lem2  8013  fin23lem14  8202  axcc2lem  8305  ttukeylem4  8381  ttukeylem7  8384  pwfseqlem2  8523  uzin  10507  xrmax1  10752  xrmax2  10753  xrmin1  10754  xrmin2  10755  max1ALT  10763  max0sub  10771  ifle  10772  xnegpnf  10784  xnegmnf  10785  xaddpnf1  10801  xaddpnf2  10802  xaddmnf1  10803  xaddmnf2  10804  pnfaddmnf  10805  mnfaddpnf  10806  xmul01  10835  xmulneg1  10837  xmulpnf1  10842  fzprval  11095  fztpval  11096  seqf1olem1  11350  seqf1olem2  11351  expnnval  11373  exp0  11374  bcval2  11584  ccatval1  11733  swrd00  11753  swrdval2  11755  ccatco  11792  max0add  12103  absmax  12121  sumrblem  12493  fsumcvg  12494  summolem2a  12497  zsum  12500  isum  12501  sumss  12506  sumss2  12508  fsumcvg2  12509  fsumser  12512  fsumsplit  12521  sumsplit  12540  ef0lem  12669  rpnnen2lem3  12804  rpnnen2lem9  12810  ruclem2  12819  ruclem3  12820  sadadd2lem2  12950  sadcf  12953  sadc0  12954  sadcp1  12955  sadcaddlem  12957  smupf  12978  smup0  12979  gcd0val  12997  eucalgf  13062  eucalginv  13063  eucalglt  13064  iserodd  13197  pc0  13216  pcgcd  13239  pcmptcl  13248  pcmpt  13249  pcmpt2  13250  pcprod  13252  fldivp1  13254  prmreclem2  13273  prmreclem4  13275  1arithlem4  13282  vdwlem6  13342  ramtcl2  13367  ramcl2  13372  ramub1lem1  13382  ressid2  13505  xpscfv  13775  xpsfrnel  13776  xpsaddlem  13788  xpsvsca  13792  setcepi  14231  gsumval1  14767  gsumval2a  14770  mulg0  14883  mulgnn  14884  dfod2  15188  oddvds2  15190  frgpuptinv  15391  frgpup2  15396  frgpup3lem  15397  cyggenod  15482  cyggex  15495  gsumzsplit  15517  dprdfid  15563  dmdprdsplitlem  15583  abvtrivd  15916  psrlidm  16455  psrridm  16456  mvrid  16475  mvrf1  16477  mplmonmul  16515  mplcoe1  16516  mplcoe3  16517  mplcoe2  16518  mplmon2  16541  subrgasclcl  16547  coe1tm  16653  coe1tmfv1  16654  coe1tmmul2fv  16658  coe1pwmulfv  16660  coe1sclmul  16662  coe1sclmul2  16664  ply1sclid  16667  znf1o  16820  zzngim  16821  obsipid  16937  2ndcdisj  17507  ptpjpre1  17591  ptbasfi  17601  ptpjopn  17632  isfcls  18029  fclscmpi  18049  ptcmplem2  18072  ptcmplem3  18073  tsmssplit  18169  dscmet  18608  dscopn  18609  xrsxmet  18828  icccmplem2  18842  cnmpt2pc  18941  iccpnfcnv  18957  xrhmeo  18959  oprpiece1res1  18964  htpycc  18993  pcoval1  19026  pcohtpylem  19032  pcopt  19035  pcopt2  19036  pcoass  19037  pcorevlem  19039  cmetcaulem  19229  ovolunlem1a  19380  ovolunlem1  19381  ovolicc1  19400  ovolicc2lem3  19403  ovolicc2lem4  19404  ioorinv  19456  ioorcl  19457  i1f1lem  19569  itg11  19571  itg1addlem2  19577  itg1addlem4  19579  i1fres  19585  itg1climres  19594  mbfi1fseqlem4  19598  mbfi1fseqlem5  19599  mbfi1fseqlem6  19600  mbfi1flim  19603  itg2const2  19621  itg2seq  19622  itg2uba  19623  itg2splitlem  19628  itg2split  19629  itg2monolem1  19630  itg2cnlem1  19641  itg2cnlem2  19642  iblcnlem  19668  iblss  19684  iblss2  19685  itgitg2  19686  itgle  19689  itgss  19691  itgss2  19692  itgss3  19694  itgless  19696  ibladdlem  19699  itgaddlem1  19702  iblabslem  19707  iblabs  19708  iblabsr  19709  iblmulc2  19710  itgspliticc  19716  bddmulibl  19718  itggt0  19721  itgcn  19722  ditgpos  19731  limcvallem  19746  ellimc2  19752  limcres  19761  limccnp  19766  limccnp2  19767  limcco  19768  dvcobr  19820  dvexp2  19828  evlslem3  19923  evlslem1  19924  ig1pval2  20084  elply2  20103  elplyd  20109  ply1termlem  20110  plyeq0lem  20117  plypf1  20119  coeeq2  20149  coe1termlem  20164  dgrcolem2  20180  dvply1  20189  plydivlem4  20201  vieta1lem2  20216  aareccl  20231  dvtaylp  20274  pserdvlem2  20332  abelthlem9  20344  logtayl  20539  0cxp  20545  cxpexp  20547  leibpilem2  20769  leibpi  20770  rlimcnp2  20793  efrlim  20796  isppw  20885  vmappw  20887  muval1  20904  isnsqf  20906  mule1  20919  sqff1o  20953  muinv  20966  chtublem  20983  dchrelbasd  21011  dchr1  21029  dchrptlem2  21037  bposlem1  21056  bposlem3  21058  bposlem5  21060  bposlem6  21061  lgsval2lem  21078  lgs0  21081  lgs2  21085  lgsneg  21091  lgsdilem  21094  lgsdir2  21100  lgsdir  21102  lgsdi  21104  lgsne0  21105  rplogsumlem2  21167  dchrvmasum2if  21179  dchrvmasumiflem1  21183  dchrisum0flblem2  21191  dchrisum0fno1  21193  rpvmasum2  21194  rplogsum  21209  pntrlog2bndlem4  21262  pntrlog2bndlem5  21263  padicabv  21312  ostth2lem4  21318  eupath2  21690  gxpval  21835  gx0  21837  ifbieq12d2  23990  elimifd  23992  elim2if  23993  partfun  24075  ofldchr  24232  xrge0iifcnv  24307  xrge0iifiso  24309  xrge0iifhom  24311  indval2  24400  ind1  24404  esumpinfval  24451  sigaclfu2  24492  ballotlemsgt1  24756  ballotlemsel1i  24758  ballotlemsi  24760  ballotlemsima  24761  ballotlemrv1  24766  lgamgulmlem4  24804  igamz  24820  indispcon  24909  cvmliftlem10  24969  prodrblem  25244  fprodcvg  25245  prodmolem2a  25249  zprod  25252  iprod  25253  iprodn0  25255  prodss  25262  fprodsplit  25278  rdgprc0  25405  dfrdg2  25407  dfrdg3  25408  unisnif  25720  dfrdg4  25745  axlowdimlem15  25843  axlowdim  25848  mblfinlem  26190  mbfposadd  26200  itg2addnclem  26202  itg2addnc  26205  itg2gt0cn  26206  ibladdnclem  26207  itgaddnclem1  26209  itgaddnclem2  26210  iblabsnclem  26214  iblabsnc  26215  iblmulc2nc  26216  bddiblnc  26221  itggt0cn  26223  areacirclem6  26233  areacirc  26234  fnejoin2  26335  sdclem1  26384  fdc  26386  heiborlem4  26460  pw2f1ocnv  27045  aomclem5  27070  kelac1  27076  uvcvv1  27153  flcidc  27294  pmtrprfv  27311  pmtrmvd  27313  pmtrfinv  27317  psgnunilem1  27331  mamulid  27373  mamurid  27374  sdrgacs  27424  phisum  27433  mon1pid  27439  refsum2cnlem1  27622  afvfundmfveq  27916  ifeqda  27988  2if2  27989  swrdltnd  28073  swrdccat3a  28105  swrdccat3b  28106  shwrdidx  28130  shwrdidxmod  28131  shwrdidxm1  28133  2shwrd1lem2  28137  2shwrd2lem1  28142  2shwrd  28146  2shwrdid  28147  2shwrdcom  28153  sgn0  28377  sgnn  28382  cdleme27a  31003  cdleme31sn1  31017  cdleme31fv1  31027  cdlemefs27cl  31049  cdlemk40t  31554  dihvalb  31874  mapdhval0  32362  hdmap1val0  32437
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-if 3732
  Copyright terms: Public domain W3C validator