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

Theorem simprrl 741
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 444 . 2  |-  ( ( ch  /\  th )  ->  ch )
21ad2antll 710 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  grpridd  6279  eroveu  6991  undom  7188  mapdom2  7270  domunfican  7371  fofinf1o  7379  finsschain  7405  wemaplem3  7509  oemapvali  7632  iunfictbso  7987  enfin2i  8193  fin1a2s  8286  ttukeylem6  8386  distrlem4pr  8895  divdivdiv  9707  divmuleq  9711  divsubdiv  9722  lediv12a  9895  xralrple  10783  seqcaopr  11352  leexp2r  11429  hashbclem  11693  rlimresb  12351  summo  12503  fsum2dlem  12546  bezoutlem3  13032  bezoutlem4  13033  qredeu  13099  pcqmul  13219  pcadd  13250  pockthg  13266  prmreclem2  13277  vdwlem10  13350  ramub1lem2  13387  mreexexlem4d  13864  mreexdomd  13866  issubc3  14038  cofucl  14077  setcmon  14234  setcepi  14235  drsdirfi  14387  poslubmo  14565  ghmpreima  15019  gaorber  15077  odcau  15230  pgpssslw  15240  fislw  15251  lsmsubm  15279  efgsfo  15363  gsum2d2  15540  pgpfac1lem5  15629  pgpfac1  15630  pgpfaclem2  15632  pgpfaclem3  15633  unitgrp  15764  lmodprop2d  15998  lsspropd  16085  lbsextlem4  16225  assapropd  16378  neiint  17160  restbas  17214  iscnp4  17319  cnpco  17323  nrmsep  17413  regsep2  17432  ordthauslem  17439  1stcfb  17500  1stcrest  17508  2ndcctbss  17510  2ndcdisj  17511  2ndcomap  17513  dis2ndc  17515  nlly2i  17531  islly2  17539  hausllycmp  17549  lly1stc  17551  ptbasin  17601  txcls  17628  ptcnp  17646  txlly  17660  txnlly  17661  txtube  17664  txcmplem1  17665  txcmplem2  17666  xkococnlem  17683  basqtop  17735  regr1lem  17763  kqreglem1  17765  kqreglem2  17766  kqnrmlem1  17767  kqnrmlem2  17768  reghmph  17817  nrmhmph  17818  opnfbas  17866  rnelfmlem  17976  fmufil  17983  fclscf  18049  fclsfnflim  18051  flimfnfcls  18052  uffclsflim  18055  cnpfcfi  18064  cnpfcf  18065  alexsubALTlem2  18071  alexsubALTlem4  18073  tgpconcompeqg  18133  ghmcnp  18136  divstgplem  18142  tsmsxp  18176  blssps  18446  blss  18447  blcld  18527  metequiv2  18532  met2ndci  18544  prdsxmslem2  18551  txmetcnp  18569  nlmvscnlem1  18714  xrge0tsms  18857  ipcnlem1  19191  iscmet3  19238  cmetss  19259  minveclem3  19322  pmltpc  19339  ovolscalem2  19402  ovolicc2lem5  19409  ovolicc2  19410  nulmbl2  19423  ioombl1  19448  uniioombllem6  19472  uniioombl  19473  vitalilem3  19494  i1faddlem  19577  mbfmullem  19609  itg2split  19633  lhop2  19891  dvfsumrlim  19907  itgsubst  19925  evlslem1  19928  plydivex  20206  plyexmo  20222  ulmbdd  20306  cxploglim  20808  dchrptlem2  21041  lgsquad2lem2  21135  2sqlem5  21144  dchrvmasumif  21189  rpvmasum2  21198  dchrisum0re  21199  dchrisum0lem3  21205  dchrisum0  21206  dchrmusum  21210  dchrvmasum  21211  pntibndlem3  21278  pntlemp  21296  ostth3  21324  cusgrafilem1  21480  ablo4  21867  smcnlem  22185  pjhthmo  22796  mdslmd1lem1  23820  xrge0tsmsd  24215  xpinpreima2  24297  qqhval2  24358  dya2iocnrect  24623  orvcgteel  24717  orvclteel  24722  derangenlem  24849  cnpcon  24909  txpcon  24911  conpcon  24914  pconpi1  24916  iccllyscon  24929  rellyscon  24930  cvmcov2  24954  cvmliftmolem2  24961  cvmliftmo  24963  cvmliftlem15  24977  cvmliftpht  24997  cvmlift3lem2  24999  relexpsucl  25124  relexpcnv  25125  relexpdm  25127  relexprn  25128  relexpadd  25130  relexpindlem  25131  rtrclreclem.trans  25138  rtrclreclem.min  25139  rtrclind  25141  dedekind  25179  prodmo  25254  fprod2dlem  25296  ax5seglem9  25868  ax5seg  25869  axcontlem8  25902  axcontlem12  25906  cgrextend  25934  btwnouttr2  25948  cgrsub  25971  cgrxfr  25981  btwnxfr  25982  colineardim1  25987  btwnconn1lem6  26018  btwnconn1lem13  26025  btwnconn1lem14  26026  btwnconn3  26029  seglecgr12im  26036  segleantisym  26041  outsideofeq  26056  outsidele  26058  lineunray  26073  linethru  26079  mblfinlem2  26235  cnambfre  26245  areacirclem6  26287  comppfsc  26378  neibastop2lem  26380  neibastop2  26381  istotbnd3  26471  sstotbnd  26475  crngm4  26604  diophin  26822  pellexlem3  26885  pellexlem5  26887  pellex  26889  pell14qrmulcl  26917  jm2.19lem3  27053  jm2.25  27061  jm2.27b  27068  lmhmfgsplit  27152  hbtlem2  27296  hbtlem5  27300  issubmd  27351  psgnunilem4  27388  psgneu  27397  fnchoice  27667  stoweidlem17  27733  stoweidlem53  27769  stoweidlem61  27777  cshwsdisj  28248  2spotiundisj  28388  cvlcvr1  30074  4atlem12  30346  paddasslem10  30563  paddasslem12  30565  paddasslem13  30566  lhpexle3lem  30745  cdlemd4  30935  cdleme0cq  30949  cdlemefs32sn1aw  31148  cdleme43fsv1snlem  31154  cdleme32d  31178  cdleme32f  31180  cdleme40m  31201  cdleme40n  31202  cdleme42keg  31220  cdleme42mgN  31222  cdleme50trn2  31285  cdleme50trn3  31287  cdlemm10N  31853  dihvalcqpre  31970  dihopelvalcpre  31983  dihmeetlem1N  32025  dihjat1lem  32163  mapd0  32400  mapdh9a  32525
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 178  df-an 361
  Copyright terms: Public domain W3C validator