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

Theorem iftrue 3705
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 2519 . 2  |-  ( ph  ->  A  =  { x  |  ( ( x  e.  B  ->  ph )  ->  ( x  e.  A  /\  ph ) ) } )
3 dfif2 3701 . 2  |-  if (
ph ,  A ,  B )  =  {
x  |  ( ( x  e.  B  ->  ph )  ->  ( x  e.  A  /\  ph ) ) }
42, 3syl6reqr 2455 1  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   {cab 2390   ifcif 3699
This theorem is referenced by:  ifsb  3708  ifbi  3716  ifeq2da  3725  ifclda  3726  elimif  3728  ifbothda  3729  ifid  3731  ifeqor  3736  ifnot  3737  ifan  3738  ifor  3739  dedth  3740  elimhyp  3747  elimhyp2v  3748  elimhyp3v  3749  elimhyp4v  3750  elimdhyp  3752  keephyp2v  3754  keephyp3v  3755  dfopif  3941  dfopg  3942  somin1  5229  somincom  5230  xpima1  5273  dfiota4  5405  elimdelov  6112  riotav  6513  riotaiota  6514  tz7.44-1  6623  tz7.44-3  6625  oe0m  6721  resixpfo  7059  boxriin  7063  boxcutc  7064  pw2f1olem  7171  unxpdomlem2  7273  unxpdomlem3  7274  ordtypelem1  7443  wemaplem2  7472  unwdomg  7508  ixpiunwdom  7515  cantnfp1lem2  7591  cantnfp1lem3  7592  acndom  7888  iunfictbso  7951  dfac12lem2  7980  fin23lem14  8169  axcc2lem  8272  ttukeylem4  8348  ttukeylem7  8351  pwfseqlem2  8490  uzin  10474  xrmax1  10719  xrmax2  10720  xrmin1  10721  xrmin2  10722  max1ALT  10730  max0sub  10738  ifle  10739  xnegpnf  10751  xnegmnf  10752  xaddpnf1  10768  xaddpnf2  10769  xaddmnf1  10770  xaddmnf2  10771  pnfaddmnf  10772  mnfaddpnf  10773  xmul01  10802  xmulneg1  10804  xmulpnf1  10809  fzprval  11062  fztpval  11063  seqf1olem1  11317  seqf1olem2  11318  expnnval  11340  exp0  11341  bcval2  11551  ccatval1  11700  swrd00  11720  swrdval2  11722  ccatco  11759  max0add  12070  absmax  12088  sumrblem  12460  fsumcvg  12461  summolem2a  12464  zsum  12467  isum  12468  sumss  12473  sumss2  12475  fsumcvg2  12476  fsumser  12479  fsumsplit  12488  sumsplit  12507  ef0lem  12636  rpnnen2lem3  12771  rpnnen2lem9  12777  ruclem2  12786  ruclem3  12787  sadadd2lem2  12917  sadcf  12920  sadc0  12921  sadcp1  12922  sadcaddlem  12924  smupf  12945  smup0  12946  gcd0val  12964  eucalgf  13029  eucalginv  13030  eucalglt  13031  iserodd  13164  pc0  13183  pcgcd  13206  pcmptcl  13215  pcmpt  13216  pcmpt2  13217  pcprod  13219  fldivp1  13221  prmreclem2  13240  prmreclem4  13242  1arithlem4  13249  vdwlem6  13309  ramtcl2  13334  ramcl2  13339  ramub1lem1  13349  ressid2  13472  xpscfv  13742  xpsfrnel  13743  xpsaddlem  13755  xpsvsca  13759  setcepi  14198  gsumval1  14734  gsumval2a  14737  mulg0  14850  mulgnn  14851  dfod2  15155  oddvds2  15157  frgpuptinv  15358  frgpup2  15363  frgpup3lem  15364  cyggenod  15449  cyggex  15462  gsumzsplit  15484  dprdfid  15530  dmdprdsplitlem  15550  abvtrivd  15883  psrlidm  16422  psrridm  16423  mvrid  16442  mvrf1  16444  mplmonmul  16482  mplcoe1  16483  mplcoe3  16484  mplcoe2  16485  mplmon2  16508  subrgasclcl  16514  coe1tm  16620  coe1tmfv1  16621  coe1tmmul2fv  16625  coe1pwmulfv  16627  coe1sclmul  16629  coe1sclmul2  16631  ply1sclid  16634  znf1o  16787  zzngim  16788  obsipid  16904  2ndcdisj  17472  ptpjpre1  17556  ptbasfi  17566  ptpjopn  17597  isfcls  17994  fclscmpi  18014  ptcmplem2  18037  ptcmplem3  18038  tsmssplit  18134  dscmet  18573  dscopn  18574  xrsxmet  18793  icccmplem2  18807  cnmpt2pc  18906  iccpnfcnv  18922  xrhmeo  18924  oprpiece1res1  18929  htpycc  18958  pcoval1  18991  pcohtpylem  18997  pcopt  19000  pcopt2  19001  pcoass  19002  pcorevlem  19004  cmetcaulem  19194  ovolunlem1a  19345  ovolunlem1  19346  ovolicc1  19365  ovolicc2lem3  19368  ovolicc2lem4  19369  ioorinv  19421  ioorcl  19422  i1f1lem  19534  itg11  19536  itg1addlem2  19542  itg1addlem4  19544  i1fres  19550  itg1climres  19559  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1fseqlem6  19565  mbfi1flim  19568  itg2const2  19586  itg2seq  19587  itg2uba  19588  itg2splitlem  19593  itg2split  19594  itg2monolem1  19595  itg2cnlem1  19606  itg2cnlem2  19607  iblcnlem  19633  iblss  19649  iblss2  19650  itgitg2  19651  itgle  19654  itgss  19656  itgss2  19657  itgss3  19659  itgless  19661  ibladdlem  19664  itgaddlem1  19667  iblabslem  19672  iblabs  19673  iblabsr  19674  iblmulc2  19675  itgspliticc  19681  bddmulibl  19683  itggt0  19686  itgcn  19687  ditgpos  19696  limcvallem  19711  ellimc2  19717  limcres  19726  limccnp  19731  limccnp2  19732  limcco  19733  dvcobr  19785  dvexp2  19793  evlslem3  19888  evlslem1  19889  ig1pval2  20049  elply2  20068  elplyd  20074  ply1termlem  20075  plyeq0lem  20082  plypf1  20084  coeeq2  20114  coe1termlem  20129  dgrcolem2  20145  dvply1  20154  plydivlem4  20166  vieta1lem2  20181  aareccl  20196  dvtaylp  20239  pserdvlem2  20297  abelthlem9  20309  logtayl  20504  0cxp  20510  cxpexp  20512  leibpilem2  20734  leibpi  20735  rlimcnp2  20758  efrlim  20761  isppw  20850  vmappw  20852  muval1  20869  isnsqf  20871  mule1  20884  sqff1o  20918  muinv  20931  chtublem  20948  dchrelbasd  20976  dchr1  20994  dchrptlem2  21002  bposlem1  21021  bposlem3  21023  bposlem5  21025  bposlem6  21026  lgsval2lem  21043  lgs0  21046  lgs2  21050  lgsneg  21056  lgsdilem  21059  lgsdir2  21065  lgsdir  21067  lgsdi  21069  lgsne0  21070  rplogsumlem2  21132  dchrvmasum2if  21144  dchrvmasumiflem1  21148  dchrisum0flblem2  21156  dchrisum0fno1  21158  rpvmasum2  21159  rplogsum  21174  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  padicabv  21277  ostth2lem4  21283  eupath2  21655  gxpval  21800  gx0  21802  ifbieq12d2  23955  elimifd  23957  elim2if  23958  partfun  24040  ofldchr  24197  xrge0iifcnv  24272  xrge0iifiso  24274  xrge0iifhom  24276  indval2  24365  ind1  24369  esumpinfval  24416  sigaclfu2  24457  ballotlemsgt1  24721  ballotlemsel1i  24723  ballotlemsi  24725  ballotlemsima  24726  ballotlemrv1  24731  lgamgulmlem4  24769  igamz  24785  indispcon  24874  cvmliftlem10  24934  prodrblem  25208  fprodcvg  25209  prodmolem2a  25213  zprod  25216  iprod  25217  iprodn0  25219  prodss  25226  fprodsplit  25242  rdgprc0  25364  dfrdg2  25366  dfrdg3  25367  unisnif  25678  dfrdg4  25703  axlowdimlem15  25799  axlowdim  25804  mblfinlem  26143  mbfposadd  26153  itg2addnclem  26155  itg2addnc  26158  itg2gt0cn  26159  ibladdnclem  26160  itgaddnclem1  26162  itgaddnclem2  26163  iblabsnclem  26167  iblabsnc  26168  iblmulc2nc  26169  bddiblnc  26174  itggt0cn  26176  areacirclem6  26186  areacirc  26187  fnejoin2  26288  sdclem1  26337  fdc  26339  heiborlem4  26413  pw2f1ocnv  26998  aomclem5  27023  kelac1  27029  uvcvv1  27106  flcidc  27247  pmtrprfv  27264  pmtrmvd  27266  pmtrfinv  27270  psgnunilem1  27284  mamulid  27326  mamurid  27327  sdrgacs  27377  phisum  27386  mon1pid  27392  refsum2cnlem1  27575  afvfundmfveq  27869  2if2  27941  swrdltnd  28000  swrdccat3a  28030  swrdccat3b  28031  sgn0  28233  sgnn  28238  cdleme27a  30849  cdleme31sn1  30863  cdleme31fv1  30873  cdlemefs27cl  30895  cdlemk40t  31400  dihvalb  31720  mapdhval0  32208  hdmap1val0  32283
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-if 3700
  Copyright terms: Public domain W3C validator