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  6060  eroveu  6753  undom  6950  mapdom2  7032  domunfican  7129  fofinf1o  7137  finsschain  7162  wemaplem3  7263  oemapvali  7386  iunfictbso  7741  enfin2i  7947  fin1a2s  8040  ttukeylem6  8141  distrlem4pr  8650  divdivdiv  9461  divmuleq  9465  divsubdiv  9476  lediv12a  9649  xralrple  10532  seqcaopr  11083  leexp2r  11159  hashbclem  11390  rlimresb  12039  summo  12190  fsum2dlem  12233  bezoutlem3  12719  bezoutlem4  12720  qredeu  12786  pcqmul  12906  pcadd  12937  pockthg  12953  prmreclem2  12964  vdwlem10  13037  ramub1lem2  13074  mreexexlem4d  13549  mreexdomd  13551  issubc3  13723  cofucl  13762  setcmon  13919  setcepi  13920  drsdirfi  14072  poslubmo  14250  ghmpreima  14704  gaorber  14762  odcau  14915  pgpssslw  14925  fislw  14936  lsmsubm  14964  efgsfo  15048  gsum2d2  15225  pgpfac1lem5  15314  pgpfac1  15315  pgpfaclem2  15317  pgpfaclem3  15318  unitgrp  15449  lmodprop2d  15687  lsspropd  15774  lbsextlem4  15914  assapropd  16067  neiint  16841  restbas  16889  cnpco  16996  nrmsep  17085  regsep2  17104  ordthauslem  17111  1stcfb  17171  1stcrest  17179  2ndcctbss  17181  2ndcdisj  17182  2ndcomap  17184  dis2ndc  17186  nlly2i  17202  islly2  17210  hausllycmp  17220  lly1stc  17222  ptbasin  17272  txcls  17299  ptcnp  17316  txlly  17330  txnlly  17331  txtube  17334  txcmplem1  17335  txcmplem2  17336  xkococnlem  17353  basqtop  17402  regr1lem  17430  kqreglem1  17432  kqreglem2  17433  kqnrmlem1  17434  kqnrmlem2  17435  reghmph  17484  nrmhmph  17485  opnfbas  17537  rnelfmlem  17647  fmufil  17654  fclscf  17720  fclsfnflim  17722  flimfnfcls  17723  uffclsflim  17726  cnpfcfi  17735  cnpfcf  17736  alexsubALTlem2  17742  alexsubALTlem4  17744  tgpconcompeqg  17794  ghmcnp  17797  divstgplem  17803  tsmsxp  17837  blss  17972  blcld  18051  metequiv2  18056  met2ndci  18068  prdsxmslem2  18075  txmetcnp  18093  nlmvscnlem1  18197  xrge0tsms  18339  ipcnlem1  18672  iscmet3  18719  cmetss  18740  minveclem3  18793  pmltpc  18810  ovolscalem2  18873  ovolicc2lem5  18880  ovolicc2  18881  nulmbl2  18894  ioombl1  18919  uniioombllem6  18943  uniioombl  18944  vitalilem3  18965  i1faddlem  19048  mbfmullem  19080  itg2split  19104  lhop2  19362  dvfsumrlim  19378  itgsubst  19396  evlslem1  19399  plydivex  19677  plyexmo  19693  ulmbdd  19775  cxploglim  20272  dchrptlem2  20504  lgsquad2lem2  20598  2sqlem5  20607  dchrvmasumif  20652  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lem3  20668  dchrisum0  20669  dchrmusum  20673  dchrvmasum  20674  pntibndlem3  20741  pntlemp  20759  ostth3  20787  ablo4  20954  smcnlem  21270  pjhthmo  21881  mdslmd1lem1  22905  xpinpreima2  23291  xrge0tsmsd  23382  orvcgteel  23668  orvclteel  23673  derangenlem  23702  cnpcon  23761  txpcon  23763  conpcon  23766  pconpi1  23768  iccllyscon  23781  rellyscon  23782  cvmcov2  23806  cvmliftmolem2  23813  cvmliftmo  23815  cvmliftlem15  23829  cvmliftpht  23849  cvmlift3lem2  23851  relexpsucl  24028  relexpcnv  24029  relexpdm  24032  relexprn  24033  relexpadd  24035  relexpindlem  24036  rtrclreclem.trans  24043  rtrclreclem.min  24044  rtrclind  24046  dedekind  24082  ax5seglem9  24565  ax5seg  24566  axcontlem8  24599  axcontlem12  24603  cgrextend  24631  btwnouttr2  24645  cgrsub  24668  cgrxfr  24678  btwnxfr  24679  colineardim1  24684  btwnconn1lem6  24715  btwnconn1lem13  24722  btwnconn1lem14  24723  btwnconn3  24726  seglecgr12im  24733  segleantisym  24738  outsideofeq  24753  outsidele  24755  lineunray  24770  linethru  24776  areacirclem6  24930  resgcom  25351  fprodsub  25379  rltrooo  25415  iscnp4  25563  comppfsc  26307  neibastop2lem  26309  neibastop2  26310  istotbnd3  26495  sstotbnd  26499  crngm4  26628  diophin  26852  pellexlem3  26916  pellexlem5  26918  pellex  26920  pell14qrmulcl  26948  jm2.19lem3  27084  jm2.25  27092  jm2.27b  27099  lmhmfgsplit  27184  hbtlem2  27328  hbtlem5  27332  issubmd  27383  psgnunilem4  27420  psgneu  27429  fnchoice  27700  stoweidlem17  27766  stoweidlem53  27802  cvlcvr1  29529  4atlem12  29801  paddasslem10  30018  paddasslem12  30020  paddasslem13  30021  lhpexle3lem  30200  cdlemd4  30390  cdleme0cq  30404  cdlemefs32sn1aw  30603  cdleme43fsv1snlem  30609  cdleme32d  30633  cdleme32f  30635  cdleme40m  30656  cdleme40n  30657  cdleme42keg  30675  cdleme42mgN  30677  cdleme50trn2  30740  cdleme50trn3  30742  cdlemm10N  31308  dihvalcqpre  31425  dihopelvalcpre  31438  dihmeetlem1N  31480  dihjat1lem  31618  mapd0  31855  mapdh9a  31980
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