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

Theorem iftrue 3647
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 2473 . 2  |-  ( ph  ->  A  =  { x  |  ( ( x  e.  B  ->  ph )  ->  ( x  e.  A  /\  ph ) ) } )
3 dfif2 3643 . 2  |-  if (
ph ,  A ,  B )  =  {
x  |  ( ( x  e.  B  ->  ph )  ->  ( x  e.  A  /\  ph ) ) }
42, 3syl6reqr 2409 1  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1642    e. wcel 1710   {cab 2344   ifcif 3641
This theorem is referenced by:  ifsb  3650  ifbi  3658  ifeq2da  3667  ifclda  3668  elimif  3670  ifbothda  3671  ifid  3673  ifeqor  3678  ifnot  3679  ifan  3680  ifor  3681  dedth  3682  elimhyp  3689  elimhyp2v  3690  elimhyp3v  3691  elimhyp4v  3692  elimdhyp  3694  keephyp2v  3696  keephyp3v  3697  dfopif  3872  dfopg  3873  somin1  5158  somincom  5159  dfiota4  5326  elimdelov  6011  riotav  6393  riotaiota  6394  tz7.44-1  6503  tz7.44-3  6505  oe0m  6601  resixpfo  6939  boxriin  6943  boxcutc  6944  pw2f1olem  7051  unxpdomlem2  7153  unxpdomlem3  7154  ordtypelem1  7320  wemaplem2  7349  unwdomg  7385  ixpiunwdom  7392  cantnfp1lem2  7468  cantnfp1lem3  7469  acndom  7765  iunfictbso  7828  dfac12lem2  7857  fin23lem14  8046  axcc2lem  8149  ttukeylem4  8226  ttukeylem7  8229  pwfseqlem2  8368  uzin  10349  xrmax1  10593  xrmax2  10594  xrmin1  10595  xrmin2  10596  max1ALT  10604  max0sub  10612  ifle  10613  xnegpnf  10625  xnegmnf  10626  xaddpnf1  10642  xaddpnf2  10643  xaddmnf1  10644  xaddmnf2  10645  pnfaddmnf  10646  mnfaddpnf  10647  xmul01  10676  xmulneg1  10678  xmulpnf1  10683  fzprval  10933  fztpval  10934  seqf1olem1  11174  seqf1olem2  11175  expnnval  11197  exp0  11198  bcval2  11408  ccatval1  11521  swrd00  11541  swrdval2  11543  ccatco  11580  max0add  11885  absmax  11903  sumrblem  12275  fsumcvg  12276  summolem2a  12279  zsum  12282  isum  12283  sumss  12288  sumss2  12290  fsumcvg2  12291  fsumser  12294  fsumsplit  12303  sumsplit  12322  ef0lem  12451  rpnnen2lem3  12586  rpnnen2lem9  12592  ruclem2  12601  ruclem3  12602  sadadd2lem2  12732  sadcf  12735  sadc0  12736  sadcp1  12737  sadcaddlem  12739  smupf  12760  smup0  12761  gcd0val  12779  eucalgf  12844  eucalginv  12845  eucalglt  12846  iserodd  12979  pc0  12998  pcgcd  13021  pcmptcl  13030  pcmpt  13031  pcmpt2  13032  pcprod  13034  fldivp1  13036  prmreclem2  13055  prmreclem4  13057  1arithlem4  13064  vdwlem6  13124  ramtcl2  13149  ramcl2  13154  ramub1lem1  13164  ressid2  13287  xpscfv  13557  xpsfrnel  13558  xpsaddlem  13570  xpsvsca  13574  setcepi  14013  gsumval1  14549  gsumval2a  14552  mulg0  14665  mulgnn  14666  dfod2  14970  oddvds2  14972  frgpuptinv  15173  frgpup2  15178  frgpup3lem  15179  cyggenod  15264  cyggex  15277  gsumzsplit  15299  dprdfid  15345  dmdprdsplitlem  15365  abvtrivd  15698  psrlidm  16241  psrridm  16242  mvrid  16261  mvrf1  16263  mplmonmul  16301  mplcoe1  16302  mplcoe3  16303  mplcoe2  16304  mplmon2  16327  subrgasclcl  16333  coe1tm  16442  coe1tmfv1  16443  coe1tmmul2fv  16447  coe1pwmulfv  16449  coe1sclmul  16451  coe1sclmul2  16453  ply1sclid  16456  znf1o  16605  zzngim  16606  obsipid  16722  2ndcdisj  17282  ptpjpre1  17366  ptbasfi  17376  ptpjopn  17406  isfcls  17800  fclscmpi  17820  ptcmplem2  17843  ptcmplem3  17844  tsmssplit  17930  dscmet  18191  dscopn  18192  xrsxmet  18411  icccmplem2  18425  cnmpt2pc  18524  iccpnfcnv  18540  xrhmeo  18542  oprpiece1res1  18547  htpycc  18576  pcoval1  18609  pcohtpylem  18615  pcopt  18618  pcopt2  18619  pcoass  18620  pcorevlem  18622  cmetcaulem  18812  ovolunlem1a  18953  ovolunlem1  18954  ovolicc1  18973  ovolicc2lem3  18976  ovolicc2lem4  18977  ioorinv  19029  ioorcl  19030  i1f1lem  19142  itg11  19144  itg1addlem2  19150  itg1addlem4  19152  i1fres  19158  itg1climres  19167  mbfi1fseqlem4  19171  mbfi1fseqlem5  19172  mbfi1fseqlem6  19173  mbfi1flim  19176  itg2const2  19194  itg2seq  19195  itg2uba  19196  itg2splitlem  19201  itg2split  19202  itg2monolem1  19203  itg2cnlem1  19214  itg2cnlem2  19215  iblcnlem  19241  iblss  19257  iblss2  19258  itgitg2  19259  itgle  19262  itgss  19264  itgss2  19265  itgss3  19267  itgless  19269  ibladdlem  19272  itgaddlem1  19275  iblabslem  19280  iblabs  19281  iblabsr  19282  iblmulc2  19283  itgspliticc  19289  bddmulibl  19291  itggt0  19294  itgcn  19295  ditgpos  19304  limcvallem  19319  ellimc2  19325  limcres  19334  limccnp  19339  limccnp2  19340  limcco  19341  dvcobr  19393  dvexp2  19401  evlslem3  19496  evlslem1  19497  ig1pval2  19657  elply2  19676  elplyd  19682  ply1termlem  19683  plyeq0lem  19690  plypf1  19692  coeeq2  19722  coe1termlem  19737  dgrcolem2  19753  dvply1  19762  plydivlem4  19774  vieta1lem2  19789  aareccl  19804  dvtaylp  19847  pserdvlem2  19905  abelthlem9  19917  logtayl  20112  0cxp  20118  cxpexp  20120  leibpilem2  20342  leibpi  20343  rlimcnp2  20366  efrlim  20369  isppw  20458  vmappw  20460  muval1  20477  isnsqf  20479  mule1  20492  sqff1o  20526  muinv  20539  chtublem  20556  dchrelbasd  20584  dchr1  20602  dchrptlem2  20610  bposlem1  20629  bposlem3  20631  bposlem5  20633  bposlem6  20634  lgsval2lem  20651  lgs0  20654  lgs2  20658  lgsneg  20664  lgsdilem  20667  lgsdir2  20673  lgsdir  20675  lgsdi  20677  lgsne0  20678  rplogsumlem2  20740  dchrvmasum2if  20752  dchrvmasumiflem1  20756  dchrisum0flblem2  20764  dchrisum0fno1  20766  rpvmasum2  20767  rplogsum  20782  pntrlog2bndlem4  20835  pntrlog2bndlem5  20836  padicabv  20885  ostth2lem4  20891  gxpval  21032  gx0  21034  ifbieq12d2  23198  elimifd  23200  elim2if  23201  xpima1  23236  partfun  23288  xrge0iifcnv  23475  xrge0iifiso  23477  xrge0iifhom  23479  indval2  23678  ind1  23682  esumpinfval  23729  sigaclfu2  23770  ballotlemsgt1  24017  ballotlemsel1i  24019  ballotlemsi  24021  ballotlemsima  24022  ballotlemrv1  24027  lgamgulmlem4  24065  igamz  24081  indispcon  24169  cvmliftlem10  24229  eupath2  24308  prodrblem  24556  fprodcvg  24557  prodmolem2a  24561  zprod  24564  iprod  24565  iprodn0  24567  prodss  24574  fprodsplit  24590  rdgprc0  24708  dfrdg2  24710  dfrdg3  24711  unisnif  25022  dfrdg4  25047  axlowdimlem15  25143  axlowdim  25148  itg2addnclem  25492  itg2addnc  25494  itg2gt0cn  25495  ibladdnclem  25496  itgaddnclem1  25498  itgaddnclem2  25499  iblabsnclem  25503  iblabsnc  25504  iblmulc2nc  25505  bddiblnc  25510  itggt0cn  25512  areacirclem6  25522  areacirc  25523  fnejoin2  25642  sdclem1  25777  fdc  25779  heiborlem4  25861  pw2f1ocnv  26453  aomclem5  26478  kelac1  26484  uvcvv1  26561  flcidc  26702  pmtrprfv  26719  pmtrmvd  26721  pmtrfinv  26725  psgnunilem1  26739  mamulid  26781  mamurid  26782  sdrgacs  26832  phisum  26841  mon1pid  26847  refsum2cnlem1  27031  afvfundmfveq  27326  sgn0  27929  sgnn  27934  cdleme27a  30608  cdleme31sn1  30622  cdleme31fv1  30632  cdlemefs27cl  30654  cdlemk40t  31159  dihvalb  31479  mapdhval0  31967  hdmap1val0  32042
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-if 3642
  Copyright terms: Public domain W3C validator