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

Theorem simprrl 773
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simprrl  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  ch )

Proof of Theorem simprrl
StepHypRef Expression
1 simpl 459 . 2  |-  ( ( ch  /\  th )  ->  ch )
21ad2antll 734 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189  df-an 373
This theorem is referenced by:  f1prex  6180  grpridd  6506  wfrlem17  7049  eroveu  7455  undom  7657  mapdom2  7740  domunfican  7841  fofinf1o  7849  finsschain  7878  wemaplem3  8060  oemapvali  8186  iunfictbso  8542  enfin2i  8748  fin1a2s  8841  ttukeylem6  8941  distrlem4pr  9448  mulcmpblnr  9492  prsrlem1  9493  dedekind  9794  divdivdiv  10305  divmuleq  10309  divsubdiv  10320  lediv12a  10496  xralrple  11495  ssfzo12bi  12003  seqcaopr  12247  leexp2r  12327  hashbclem  12612  wrd2ind  12829  rtrclreclem3  13116  rtrclreclem4  13117  relexpindlem  13119  rtrclind  13121  rlimresb  13622  summo  13776  fsum2dlem  13824  prodmo  13983  fprod2dlem  14027  bezoutlem3OLD  14498  bezoutlem4OLD  14499  bezoutlem3  14501  bezoutlem4  14502  ncoprmgcdne1b  14648  qredeu  14657  coprmproddvdslem  14672  pcqmul  14796  pcadd  14827  pockthg  14843  prmreclem2  14854  vdwlem10  14933  ramub1lem2  14978  prmgaplem6  15019  prmgaplem7  15020  cshwsdisj  15062  mreexexlem4d  15546  mreexdomd  15548  issubc3  15747  cofucl  15786  setcmon  15975  setcepi  15976  drsdirfi  16176  poslubmo  16385  posglbmo  16386  issubmd  16589  mrcmndind  16606  ghmpreima  16897  gaorber  16955  psgnunilem4  17131  psgneu  17140  odcau  17249  pgpssslw  17259  fislw  17270  lsmsubm  17298  efgsfo  17382  gsum2d2  17599  pgpfac1lem5  17705  pgpfac1  17706  pgpfaclem2  17708  pgpfaclem3  17709  unitgrp  17888  lmodprop2d  18143  lsspropd  18233  lbsextlem4  18377  assapropd  18544  evlslem1  18731  mdetunilem8  19637  mdetuni0  19639  mdetmul  19641  neiint  20113  restbas  20167  iscnp4  20272  cnpco  20276  nrmsep  20366  regsep2  20385  ordthauslem  20392  1stcfb  20453  1stcrest  20461  2ndcctbss  20463  2ndcdisj  20464  2ndcomap  20466  dis2ndc  20468  nlly2i  20484  islly2  20492  hausllycmp  20502  lly1stc  20504  comppfsc  20540  ptbasin  20585  txcls  20612  ptcnp  20630  txlly  20644  txnlly  20645  txtube  20648  txcmplem1  20649  txcmplem2  20650  xkococnlem  20667  basqtop  20719  regr1lem  20747  kqreglem1  20749  kqreglem2  20750  kqnrmlem1  20751  kqnrmlem2  20752  reghmph  20801  nrmhmph  20802  opnfbas  20850  rnelfmlem  20960  fmufil  20967  fclscf  21033  fclsfnflim  21035  flimfnfcls  21036  uffclsflim  21039  cnpfcfi  21048  cnpfcf  21049  alexsubALTlem2  21056  alexsubALTlem4  21058  tgpconcompeqg  21119  ghmcnp  21122  qustgplem  21128  tsmsxp  21162  blssps  21432  blss  21433  blcld  21513  metequiv2  21518  met2ndci  21530  prdsxmslem2  21537  txmetcnp  21555  nlmvscnlem1  21682  xrge0tsms  21845  ipcnlem1  22209  iscmet3  22256  cmetss  22277  minveclem3  22364  minveclem3OLD  22376  pmltpc  22394  ovolscalem2  22460  ovolicc2lem5  22468  ovolicc2  22469  nulmbl2  22483  ioombl1  22508  uniioombllem6  22539  uniioombl  22540  vitalilem3  22561  i1faddlem  22644  mbfmullem  22676  itg2split  22700  lhop2  22960  dvfsumrlim  22976  itgsubst  22994  plydivex  23243  plyexmo  23259  ulmbdd  23346  cxploglim  23896  dchrptlem2  24186  lgsquad2lem2  24280  2sqlem5  24289  dchrvmasumif  24334  rpvmasum2  24343  dchrisum0re  24344  dchrisum0lem3  24350  dchrisum0  24351  dchrmusum  24355  dchrvmasum  24356  pntibndlem3  24423  pntlemp  24441  ostth3  24469  legtrid  24629  hlcgreu  24656  mirreu3  24692  midexlem  24730  opphllem  24770  mideulem  24771  opphllem1  24782  oppperpex  24788  lnperpex  24838  trgcopy  24839  iscgra1  24845  cgraswap  24855  cgracom  24857  cgratr  24858  acopyeu  24868  ax5seglem9  24960  ax5seg  24961  axcontlem8  24994  axcontlem12  24998  cusgrafilem1  25200  2spotiundisj  25783  ablo4  26008  smcnlem  26326  pjhthmo  26948  mdslmd1lem1  27971  xrge0tsmsd  28541  locfinref  28661  xpinpreima2  28706  qqhval2  28779  dya2iocnrect  29096  orvcgteel  29293  orvclteel  29298  derangenlem  29887  cnpcon  29946  txpcon  29948  conpcon  29951  pconpi1  29953  iccllyscon  29966  rellyscon  29967  cvmcov2  29991  cvmliftmolem2  29998  cvmliftmo  30000  cvmliftlem15  30014  cvmliftpht  30034  cvmlift3lem2  30036  cgrextend  30768  btwnouttr2  30782  cgrsub  30805  cgrxfr  30815  btwnxfr  30816  colineardim1  30821  btwnconn1lem6  30852  btwnconn1lem13  30859  btwnconn1lem14  30860  btwnconn3  30863  seglecgr12im  30870  segleantisym  30875  outsideofeq  30890  outsidele  30892  lineunray  30907  linethru  30913  fnessref  31006  neibastop2lem  31009  neibastop2  31010  bj-finsumval0  31695  isbasisrelowllem1  31751  isbasisrelowllem2  31752  mblfinlem3  31972  cnambfre  31982  areacirclem5  32029  istotbnd3  32096  sstotbnd  32100  crngm4  32229  cvlcvr1  32899  4atlem12  33171  paddasslem10  33388  paddasslem12  33390  paddasslem13  33391  lhpexle3lem  33570  cdlemd4  33761  cdleme0cq  33775  cdlemefs32sn1aw  33975  cdleme43fsv1snlem  33981  cdleme32d  34005  cdleme32f  34007  cdleme40m  34028  cdleme40n  34029  cdleme42keg  34047  cdleme42mgN  34049  cdleme50trn2  34112  cdleme50trn3  34114  cdlemm10N  34680  dihvalcqpre  34797  dihopelvalcpre  34810  dihmeetlem1N  34852  dihjat1lem  34990  mapd0  35227  mapdh9a  35352  diophin  35609  pellexlem3  35669  pellexlem5  35671  pellex  35673  pell14qrmulcl  35703  jm2.19lem3  35840  jm2.25  35848  jm2.27b  35855  lmhmfgsplit  35938  hbtlem2  35977  hbtlem5  35981  gsumws3  36642  gsumws4  36643  fnchoice  37344  stoweidlem17  37871  stoweidlem53  37908  stoweidlem61  37916  qndenserrnbllem  38157  bgoldbtbnd  38898  rabsubmgmd  39778  lindslinindsimp1  40237
  Copyright terms: Public domain W3C validator