MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simprrl 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  6227  eroveu  6936  undom  7133  mapdom2  7215  domunfican  7316  fofinf1o  7324  finsschain  7349  wemaplem3  7451  oemapvali  7574  iunfictbso  7929  enfin2i  8135  fin1a2s  8228  ttukeylem6  8328  distrlem4pr  8837  divdivdiv  9648  divmuleq  9652  divsubdiv  9663  lediv12a  9836  xralrple  10724  seqcaopr  11288  leexp2r  11365  hashbclem  11629  rlimresb  12287  summo  12439  fsum2dlem  12482  bezoutlem3  12968  bezoutlem4  12969  qredeu  13035  pcqmul  13155  pcadd  13186  pockthg  13202  prmreclem2  13213  vdwlem10  13286  ramub1lem2  13323  mreexexlem4d  13800  mreexdomd  13802  issubc3  13974  cofucl  14013  setcmon  14170  setcepi  14171  drsdirfi  14323  poslubmo  14501  ghmpreima  14955  gaorber  15013  odcau  15166  pgpssslw  15176  fislw  15187  lsmsubm  15215  efgsfo  15299  gsum2d2  15476  pgpfac1lem5  15565  pgpfac1  15566  pgpfaclem2  15568  pgpfaclem3  15569  unitgrp  15700  lmodprop2d  15934  lsspropd  16021  lbsextlem4  16161  assapropd  16314  neiint  17092  restbas  17145  iscnp4  17250  cnpco  17254  nrmsep  17344  regsep2  17363  ordthauslem  17370  1stcfb  17430  1stcrest  17438  2ndcctbss  17440  2ndcdisj  17441  2ndcomap  17443  dis2ndc  17445  nlly2i  17461  islly2  17469  hausllycmp  17479  lly1stc  17481  ptbasin  17531  txcls  17558  ptcnp  17576  txlly  17590  txnlly  17591  txtube  17594  txcmplem1  17595  txcmplem2  17596  xkococnlem  17613  basqtop  17665  regr1lem  17693  kqreglem1  17695  kqreglem2  17696  kqnrmlem1  17697  kqnrmlem2  17698  reghmph  17747  nrmhmph  17748  opnfbas  17796  rnelfmlem  17906  fmufil  17913  fclscf  17979  fclsfnflim  17981  flimfnfcls  17982  uffclsflim  17985  cnpfcfi  17994  cnpfcf  17995  alexsubALTlem2  18001  alexsubALTlem4  18003  tgpconcompeqg  18063  ghmcnp  18066  divstgplem  18072  tsmsxp  18106  blss  18347  blcld  18426  metequiv2  18431  met2ndci  18443  prdsxmslem2  18450  txmetcnp  18468  nlmvscnlem1  18594  xrge0tsms  18737  ipcnlem1  19071  iscmet3  19118  cmetss  19139  minveclem3  19198  pmltpc  19215  ovolscalem2  19278  ovolicc2lem5  19285  ovolicc2  19286  nulmbl2  19299  ioombl1  19324  uniioombllem6  19348  uniioombl  19349  vitalilem3  19370  i1faddlem  19453  mbfmullem  19485  itg2split  19509  lhop2  19767  dvfsumrlim  19783  itgsubst  19801  evlslem1  19804  plydivex  20082  plyexmo  20098  ulmbdd  20182  cxploglim  20684  dchrptlem2  20917  lgsquad2lem2  21011  2sqlem5  21020  dchrvmasumif  21065  rpvmasum2  21074  dchrisum0re  21075  dchrisum0lem3  21081  dchrisum0  21082  dchrmusum  21086  dchrvmasum  21087  pntibndlem3  21154  pntlemp  21172  ostth3  21200  cusgrafilem1  21355  ablo4  21724  smcnlem  22042  pjhthmo  22653  mdslmd1lem1  23677  xrge0tsmsd  24053  xpinpreima2  24110  qqhval2  24166  dya2iocnrect  24426  orvcgteel  24505  orvclteel  24510  derangenlem  24637  cnpcon  24697  txpcon  24699  conpcon  24702  pconpi1  24704  iccllyscon  24717  rellyscon  24718  cvmcov2  24742  cvmliftmolem2  24749  cvmliftmo  24751  cvmliftlem15  24765  cvmliftpht  24785  cvmlift3lem2  24787  relexpsucl  24912  relexpcnv  24913  relexpdm  24915  relexprn  24916  relexpadd  24918  relexpindlem  24919  rtrclreclem.trans  24926  rtrclreclem.min  24927  rtrclind  24929  dedekind  24967  prodmo  25042  ax5seglem9  25591  ax5seg  25592  axcontlem8  25625  axcontlem12  25629  cgrextend  25657  btwnouttr2  25671  cgrsub  25694  cgrxfr  25704  btwnxfr  25705  colineardim1  25710  btwnconn1lem6  25741  btwnconn1lem13  25748  btwnconn1lem14  25749  btwnconn3  25752  seglecgr12im  25759  segleantisym  25764  outsideofeq  25779  outsidele  25781  lineunray  25796  linethru  25802  areacirclem6  25988  comppfsc  26079  neibastop2lem  26081  neibastop2  26082  istotbnd3  26172  sstotbnd  26176  crngm4  26305  diophin  26523  pellexlem3  26586  pellexlem5  26588  pellex  26590  pell14qrmulcl  26618  jm2.19lem3  26754  jm2.25  26762  jm2.27b  26769  lmhmfgsplit  26854  hbtlem2  26998  hbtlem5  27002  issubmd  27053  psgnunilem4  27090  psgneu  27099  fnchoice  27369  stoweidlem17  27435  stoweidlem53  27471  stoweidlem61  27479  cvlcvr1  29455  4atlem12  29727  paddasslem10  29944  paddasslem12  29946  paddasslem13  29947  lhpexle3lem  30126  cdlemd4  30316  cdleme0cq  30330  cdlemefs32sn1aw  30529  cdleme43fsv1snlem  30535  cdleme32d  30559  cdleme32f  30561  cdleme40m  30582  cdleme40n  30583  cdleme42keg  30601  cdleme42mgN  30603  cdleme50trn2  30666  cdleme50trn3  30668  cdlemm10N  31234  dihvalcqpre  31351  dihopelvalcpre  31364  dihmeetlem1N  31406  dihjat1lem  31544  mapd0  31781  mapdh9a  31906
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