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

Theorem simprrl 772
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 458 . 2  |-  ( ( ch  /\  th )  ->  ch )
21ad2antll 733 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  f1prex  6188  grpridd  6514  wfrlem17  7051  eroveu  7457  undom  7657  mapdom2  7740  domunfican  7841  fofinf1o  7849  finsschain  7878  wemaplem3  8054  oemapvali  8179  iunfictbso  8534  enfin2i  8740  fin1a2s  8833  ttukeylem6  8933  distrlem4pr  9440  mulcmpblnr  9484  prsrlem1  9485  dedekind  9786  divdivdiv  10297  divmuleq  10301  divsubdiv  10312  lediv12a  10488  xralrple  11487  ssfzo12bi  11992  seqcaopr  12236  leexp2r  12316  hashbclem  12599  wrd2ind  12808  rtrclreclem3  13091  rtrclreclem4  13092  relexpindlem  13094  rtrclind  13096  rlimresb  13596  summo  13750  fsum2dlem  13798  prodmo  13957  fprod2dlem  14001  bezoutlem3  14468  bezoutlem4  14469  ncoprmgcdne1b  14615  qredeu  14624  coprmproddvdslem  14639  pcqmul  14763  pcadd  14794  pockthg  14810  prmreclem2  14821  vdwlem10  14900  ramub1lem2  14945  prmgaplem6  14986  prmgaplem7  14987  cshwsdisj  15029  mreexexlem4d  15505  mreexdomd  15507  issubc3  15706  cofucl  15745  setcmon  15934  setcepi  15935  drsdirfi  16135  poslubmo  16344  posglbmo  16345  issubmd  16548  mrcmndind  16565  ghmpreima  16856  gaorber  16914  psgnunilem4  17090  psgneu  17099  odcau  17197  pgpssslw  17207  fislw  17218  lsmsubm  17246  efgsfo  17330  gsum2d2  17547  pgpfac1lem5  17653  pgpfac1  17654  pgpfaclem2  17656  pgpfaclem3  17657  unitgrp  17836  lmodprop2d  18091  lsspropd  18181  lbsextlem4  18325  assapropd  18492  evlslem1  18679  mdetunilem8  19581  mdetuni0  19583  mdetmul  19585  neiint  20057  restbas  20111  iscnp4  20216  cnpco  20220  nrmsep  20310  regsep2  20329  ordthauslem  20336  1stcfb  20397  1stcrest  20405  2ndcctbss  20407  2ndcdisj  20408  2ndcomap  20410  dis2ndc  20412  nlly2i  20428  islly2  20436  hausllycmp  20446  lly1stc  20448  comppfsc  20484  ptbasin  20529  txcls  20556  ptcnp  20574  txlly  20588  txnlly  20589  txtube  20592  txcmplem1  20593  txcmplem2  20594  xkococnlem  20611  basqtop  20663  regr1lem  20691  kqreglem1  20693  kqreglem2  20694  kqnrmlem1  20695  kqnrmlem2  20696  reghmph  20745  nrmhmph  20746  opnfbas  20794  rnelfmlem  20904  fmufil  20911  fclscf  20977  fclsfnflim  20979  flimfnfcls  20980  uffclsflim  20983  cnpfcfi  20992  cnpfcf  20993  alexsubALTlem2  21000  alexsubALTlem4  21002  tgpconcompeqg  21063  ghmcnp  21066  qustgplem  21072  tsmsxp  21106  blssps  21376  blss  21377  blcld  21457  metequiv2  21462  met2ndci  21474  prdsxmslem2  21481  txmetcnp  21499  nlmvscnlem1  21626  xrge0tsms  21789  ipcnlem1  22135  iscmet3  22182  cmetss  22203  minveclem3  22290  pmltpc  22308  ovolscalem2  22374  ovolicc2lem5  22382  ovolicc2  22383  nulmbl2  22397  ioombl1  22422  uniioombllem6  22453  uniioombl  22454  vitalilem3  22475  i1faddlem  22558  mbfmullem  22590  itg2split  22614  lhop2  22874  dvfsumrlim  22890  itgsubst  22908  plydivex  23157  plyexmo  23173  ulmbdd  23257  cxploglim  23807  dchrptlem2  24095  lgsquad2lem2  24189  2sqlem5  24198  dchrvmasumif  24243  rpvmasum2  24252  dchrisum0re  24253  dchrisum0lem3  24259  dchrisum0  24260  dchrmusum  24264  dchrvmasum  24265  pntibndlem3  24332  pntlemp  24350  ostth3  24378  legtrid  24535  hlcgreu  24562  mirreu3  24598  midexlem  24633  opphllem  24673  mideulem  24674  opphllem1  24685  oppperpex  24691  lnperpex  24741  trgcopy  24742  iscgra1  24748  cgraswap  24758  cgracom  24760  cgratr  24761  acopyeu  24768  ax5seglem9  24854  ax5seg  24855  axcontlem8  24888  axcontlem12  24892  cusgrafilem1  25093  2spotiundisj  25676  ablo4  25901  smcnlem  26219  pjhthmo  26831  mdslmd1lem1  27854  xrge0tsmsd  28428  locfinref  28548  xpinpreima2  28593  qqhval2  28666  dya2iocnrect  28983  orvcgteel  29167  orvclteel  29172  derangenlem  29723  cnpcon  29782  txpcon  29784  conpcon  29787  pconpi1  29789  iccllyscon  29802  rellyscon  29803  cvmcov2  29827  cvmliftmolem2  29834  cvmliftmo  29836  cvmliftlem15  29850  cvmliftpht  29870  cvmlift3lem2  29872  cgrextend  30601  btwnouttr2  30615  cgrsub  30638  cgrxfr  30648  btwnxfr  30649  colineardim1  30654  btwnconn1lem6  30685  btwnconn1lem13  30692  btwnconn1lem14  30693  btwnconn3  30696  seglecgr12im  30703  segleantisym  30708  outsideofeq  30723  outsidele  30725  lineunray  30740  linethru  30746  fnessref  30839  neibastop2lem  30842  neibastop2  30843  bj-finsumval0  31488  isbasisrelowllem1  31533  isbasisrelowllem2  31534  mblfinlem3  31727  cnambfre  31737  areacirclem5  31784  istotbnd3  31851  sstotbnd  31855  crngm4  31984  cvlcvr1  32658  4atlem12  32930  paddasslem10  33147  paddasslem12  33149  paddasslem13  33150  lhpexle3lem  33329  cdlemd4  33520  cdleme0cq  33534  cdlemefs32sn1aw  33734  cdleme43fsv1snlem  33740  cdleme32d  33764  cdleme32f  33766  cdleme40m  33787  cdleme40n  33788  cdleme42keg  33806  cdleme42mgN  33808  cdleme50trn2  33871  cdleme50trn3  33873  cdlemm10N  34439  dihvalcqpre  34556  dihopelvalcpre  34569  dihmeetlem1N  34611  dihjat1lem  34749  mapd0  34986  mapdh9a  35111  diophin  35368  pellexlem3  35429  pellexlem5  35431  pellex  35433  pell14qrmulcl  35463  jm2.19lem3  35600  jm2.25  35608  jm2.27b  35615  lmhmfgsplit  35698  hbtlem2  35737  hbtlem5  35741  gsumws3  36333  gsumws4  36334  fnchoice  37038  stoweidlem17  37494  stoweidlem53  37531  stoweidlem61  37539  bgoldbtbnd  38351  rabsubmgmd  38606  lindslinindsimp1  39067
  Copyright terms: Public domain W3C validator