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  6062  eroveu  6755  undom  6952  mapdom2  7034  domunfican  7131  fofinf1o  7139  finsschain  7164  wemaplem3  7265  oemapvali  7388  iunfictbso  7743  enfin2i  7949  fin1a2s  8042  ttukeylem6  8143  distrlem4pr  8652  divdivdiv  9463  divmuleq  9467  divsubdiv  9478  lediv12a  9651  xralrple  10534  seqcaopr  11085  leexp2r  11161  hashbclem  11392  rlimresb  12041  summo  12192  fsum2dlem  12235  bezoutlem3  12721  bezoutlem4  12722  qredeu  12788  pcqmul  12908  pcadd  12939  pockthg  12955  prmreclem2  12966  vdwlem10  13039  ramub1lem2  13076  mreexexlem4d  13551  mreexdomd  13553  issubc3  13725  cofucl  13764  setcmon  13921  setcepi  13922  drsdirfi  14074  poslubmo  14252  ghmpreima  14706  gaorber  14764  odcau  14917  pgpssslw  14927  fislw  14938  lsmsubm  14966  efgsfo  15050  gsum2d2  15227  pgpfac1lem5  15316  pgpfac1  15317  pgpfaclem2  15319  pgpfaclem3  15320  unitgrp  15451  lmodprop2d  15689  lsspropd  15776  lbsextlem4  15916  assapropd  16069  neiint  16843  restbas  16891  cnpco  16998  nrmsep  17087  regsep2  17106  ordthauslem  17113  1stcfb  17173  1stcrest  17181  2ndcctbss  17183  2ndcdisj  17184  2ndcomap  17186  dis2ndc  17188  nlly2i  17204  islly2  17212  hausllycmp  17222  lly1stc  17224  ptbasin  17274  txcls  17301  ptcnp  17318  txlly  17332  txnlly  17333  txtube  17336  txcmplem1  17337  txcmplem2  17338  xkococnlem  17355  basqtop  17404  regr1lem  17432  kqreglem1  17434  kqreglem2  17435  kqnrmlem1  17436  kqnrmlem2  17437  reghmph  17486  nrmhmph  17487  opnfbas  17539  rnelfmlem  17649  fmufil  17656  fclscf  17722  fclsfnflim  17724  flimfnfcls  17725  uffclsflim  17728  cnpfcfi  17737  cnpfcf  17738  alexsubALTlem2  17744  alexsubALTlem4  17746  tgpconcompeqg  17796  ghmcnp  17799  divstgplem  17805  tsmsxp  17839  blss  17974  blcld  18053  metequiv2  18058  met2ndci  18070  prdsxmslem2  18077  txmetcnp  18095  nlmvscnlem1  18199  xrge0tsms  18341  ipcnlem1  18674  iscmet3  18721  cmetss  18742  minveclem3  18795  pmltpc  18812  ovolscalem2  18875  ovolicc2lem5  18882  ovolicc2  18883  nulmbl2  18896  ioombl1  18921  uniioombllem6  18945  uniioombl  18946  vitalilem3  18967  i1faddlem  19050  mbfmullem  19082  itg2split  19106  lhop2  19364  dvfsumrlim  19380  itgsubst  19398  evlslem1  19401  plydivex  19679  plyexmo  19695  ulmbdd  19777  cxploglim  20274  dchrptlem2  20506  lgsquad2lem2  20600  2sqlem5  20609  dchrvmasumif  20654  rpvmasum2  20663  dchrisum0re  20664  dchrisum0lem3  20670  dchrisum0  20671  dchrmusum  20675  dchrvmasum  20676  pntibndlem3  20743  pntlemp  20761  ostth3  20789  ablo4  20956  smcnlem  21272  pjhthmo  21883  mdslmd1lem1  22907  xpinpreima2  23293  xrge0tsmsd  23384  orvcgteel  23670  orvclteel  23675  derangenlem  23704  cnpcon  23763  txpcon  23765  conpcon  23768  pconpi1  23770  iccllyscon  23783  rellyscon  23784  cvmcov2  23808  cvmliftmolem2  23815  cvmliftmo  23817  cvmliftlem15  23831  cvmliftpht  23851  cvmlift3lem2  23853  relexpsucl  24030  relexpcnv  24031  relexpdm  24034  relexprn  24035  relexpadd  24037  relexpindlem  24038  rtrclreclem.trans  24045  rtrclreclem.min  24046  rtrclind  24048  dedekind  24084  ax5seglem9  24567  ax5seg  24568  axcontlem8  24601  axcontlem12  24605  cgrextend  24633  btwnouttr2  24647  cgrsub  24670  cgrxfr  24680  btwnxfr  24681  colineardim1  24686  btwnconn1lem6  24717  btwnconn1lem13  24724  btwnconn1lem14  24725  btwnconn3  24728  seglecgr12im  24735  segleantisym  24740  outsideofeq  24755  outsidele  24757  lineunray  24772  linethru  24778  areacirclem6  24941  resgcom  25362  fprodsub  25390  rltrooo  25426  iscnp4  25574  comppfsc  26318  neibastop2lem  26320  neibastop2  26321  istotbnd3  26506  sstotbnd  26510  crngm4  26639  diophin  26863  pellexlem3  26927  pellexlem5  26929  pellex  26931  pell14qrmulcl  26959  jm2.19lem3  27095  jm2.25  27103  jm2.27b  27110  lmhmfgsplit  27195  hbtlem2  27339  hbtlem5  27343  issubmd  27394  psgnunilem4  27431  psgneu  27440  fnchoice  27711  stoweidlem17  27777  stoweidlem53  27813  cvlcvr1  29602  4atlem12  29874  paddasslem10  30091  paddasslem12  30093  paddasslem13  30094  lhpexle3lem  30273  cdlemd4  30463  cdleme0cq  30477  cdlemefs32sn1aw  30676  cdleme43fsv1snlem  30682  cdleme32d  30706  cdleme32f  30708  cdleme40m  30729  cdleme40n  30730  cdleme42keg  30748  cdleme42mgN  30750  cdleme50trn2  30813  cdleme50trn3  30815  cdlemm10N  31381  dihvalcqpre  31498  dihopelvalcpre  31511  dihmeetlem1N  31553  dihjat1lem  31691  mapd0  31928  mapdh9a  32053
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