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

Theorem simprrl 740
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 443 . 2  |-  ( ( ch  /\  th )  ->  ch )
21ad2antll 709 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  grpridd  6076  eroveu  6769  undom  6966  mapdom2  7048  domunfican  7145  fofinf1o  7153  finsschain  7178  wemaplem3  7279  oemapvali  7402  iunfictbso  7757  enfin2i  7963  fin1a2s  8056  ttukeylem6  8157  distrlem4pr  8666  divdivdiv  9477  divmuleq  9481  divsubdiv  9492  lediv12a  9665  xralrple  10548  seqcaopr  11099  leexp2r  11175  hashbclem  11406  rlimresb  12055  summo  12206  fsum2dlem  12249  bezoutlem3  12735  bezoutlem4  12736  qredeu  12802  pcqmul  12922  pcadd  12953  pockthg  12969  prmreclem2  12980  vdwlem10  13053  ramub1lem2  13090  mreexexlem4d  13565  mreexdomd  13567  issubc3  13739  cofucl  13778  setcmon  13935  setcepi  13936  drsdirfi  14088  poslubmo  14266  ghmpreima  14720  gaorber  14778  odcau  14931  pgpssslw  14941  fislw  14952  lsmsubm  14980  efgsfo  15064  gsum2d2  15241  pgpfac1lem5  15330  pgpfac1  15331  pgpfaclem2  15333  pgpfaclem3  15334  unitgrp  15465  lmodprop2d  15703  lsspropd  15790  lbsextlem4  15930  assapropd  16083  neiint  16857  restbas  16905  cnpco  17012  nrmsep  17101  regsep2  17120  ordthauslem  17127  1stcfb  17187  1stcrest  17195  2ndcctbss  17197  2ndcdisj  17198  2ndcomap  17200  dis2ndc  17202  nlly2i  17218  islly2  17226  hausllycmp  17236  lly1stc  17238  ptbasin  17288  txcls  17315  ptcnp  17332  txlly  17346  txnlly  17347  txtube  17350  txcmplem1  17351  txcmplem2  17352  xkococnlem  17369  basqtop  17418  regr1lem  17446  kqreglem1  17448  kqreglem2  17449  kqnrmlem1  17450  kqnrmlem2  17451  reghmph  17500  nrmhmph  17501  opnfbas  17553  rnelfmlem  17663  fmufil  17670  fclscf  17736  fclsfnflim  17738  flimfnfcls  17739  uffclsflim  17742  cnpfcfi  17751  cnpfcf  17752  alexsubALTlem2  17758  alexsubALTlem4  17760  tgpconcompeqg  17810  ghmcnp  17813  divstgplem  17819  tsmsxp  17853  blss  17988  blcld  18067  metequiv2  18072  met2ndci  18084  prdsxmslem2  18091  txmetcnp  18109  nlmvscnlem1  18213  xrge0tsms  18355  ipcnlem1  18688  iscmet3  18735  cmetss  18756  minveclem3  18809  pmltpc  18826  ovolscalem2  18889  ovolicc2lem5  18896  ovolicc2  18897  nulmbl2  18910  ioombl1  18935  uniioombllem6  18959  uniioombl  18960  vitalilem3  18981  i1faddlem  19064  mbfmullem  19096  itg2split  19120  lhop2  19378  dvfsumrlim  19394  itgsubst  19412  evlslem1  19415  plydivex  19693  plyexmo  19709  ulmbdd  19791  cxploglim  20288  dchrptlem2  20520  lgsquad2lem2  20614  2sqlem5  20623  dchrvmasumif  20668  rpvmasum2  20677  dchrisum0re  20678  dchrisum0lem3  20684  dchrisum0  20685  dchrmusum  20689  dchrvmasum  20690  pntibndlem3  20757  pntlemp  20775  ostth3  20803  ablo4  20970  smcnlem  21286  pjhthmo  21897  mdslmd1lem1  22921  xpinpreima2  23306  xrge0tsmsd  23397  orvcgteel  23683  orvclteel  23688  derangenlem  23717  cnpcon  23776  txpcon  23778  conpcon  23781  pconpi1  23783  iccllyscon  23796  rellyscon  23797  cvmcov2  23821  cvmliftmolem2  23828  cvmliftmo  23830  cvmliftlem15  23844  cvmliftpht  23864  cvmlift3lem2  23866  relexpsucl  24043  relexpcnv  24044  relexpdm  24047  relexprn  24048  relexpadd  24050  relexpindlem  24051  rtrclreclem.trans  24058  rtrclreclem.min  24059  rtrclind  24061  dedekind  24097  prodmo  24159  ax5seglem9  24637  ax5seg  24638  axcontlem8  24671  axcontlem12  24675  cgrextend  24703  btwnouttr2  24717  cgrsub  24740  cgrxfr  24750  btwnxfr  24751  colineardim1  24756  btwnconn1lem6  24787  btwnconn1lem13  24794  btwnconn1lem14  24795  btwnconn3  24798  seglecgr12im  24805  segleantisym  24810  outsideofeq  24825  outsidele  24827  lineunray  24842  linethru  24848  areacirclem6  25033  resgcom  25454  fprodsub  25482  rltrooo  25518  iscnp4  25666  comppfsc  26410  neibastop2lem  26412  neibastop2  26413  istotbnd3  26598  sstotbnd  26602  crngm4  26731  diophin  26955  pellexlem3  27019  pellexlem5  27021  pellex  27023  pell14qrmulcl  27051  jm2.19lem3  27187  jm2.25  27195  jm2.27b  27202  lmhmfgsplit  27287  hbtlem2  27431  hbtlem5  27435  issubmd  27486  psgnunilem4  27523  psgneu  27532  fnchoice  27803  stoweidlem17  27869  stoweidlem53  27905  cvlcvr1  30151  4atlem12  30423  paddasslem10  30640  paddasslem12  30642  paddasslem13  30643  lhpexle3lem  30822  cdlemd4  31012  cdleme0cq  31026  cdlemefs32sn1aw  31225  cdleme43fsv1snlem  31231  cdleme32d  31255  cdleme32f  31257  cdleme40m  31278  cdleme40n  31279  cdleme42keg  31297  cdleme42mgN  31299  cdleme50trn2  31362  cdleme50trn3  31364  cdlemm10N  31930  dihvalcqpre  32047  dihopelvalcpre  32060  dihmeetlem1N  32102  dihjat1lem  32240  mapd0  32477  mapdh9a  32602
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator