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  6246  eroveu  6958  undom  7155  mapdom2  7237  domunfican  7338  fofinf1o  7346  finsschain  7371  wemaplem3  7473  oemapvali  7596  iunfictbso  7951  enfin2i  8157  fin1a2s  8250  ttukeylem6  8350  distrlem4pr  8859  divdivdiv  9671  divmuleq  9675  divsubdiv  9686  lediv12a  9859  xralrple  10747  seqcaopr  11315  leexp2r  11392  hashbclem  11656  rlimresb  12314  summo  12466  fsum2dlem  12509  bezoutlem3  12995  bezoutlem4  12996  qredeu  13062  pcqmul  13182  pcadd  13213  pockthg  13229  prmreclem2  13240  vdwlem10  13313  ramub1lem2  13350  mreexexlem4d  13827  mreexdomd  13829  issubc3  14001  cofucl  14040  setcmon  14197  setcepi  14198  drsdirfi  14350  poslubmo  14528  ghmpreima  14982  gaorber  15040  odcau  15193  pgpssslw  15203  fislw  15214  lsmsubm  15242  efgsfo  15326  gsum2d2  15503  pgpfac1lem5  15592  pgpfac1  15593  pgpfaclem2  15595  pgpfaclem3  15596  unitgrp  15727  lmodprop2d  15961  lsspropd  16048  lbsextlem4  16188  assapropd  16341  neiint  17123  restbas  17176  iscnp4  17281  cnpco  17285  nrmsep  17375  regsep2  17394  ordthauslem  17401  1stcfb  17461  1stcrest  17469  2ndcctbss  17471  2ndcdisj  17472  2ndcomap  17474  dis2ndc  17476  nlly2i  17492  islly2  17500  hausllycmp  17510  lly1stc  17512  ptbasin  17562  txcls  17589  ptcnp  17607  txlly  17621  txnlly  17622  txtube  17625  txcmplem1  17626  txcmplem2  17627  xkococnlem  17644  basqtop  17696  regr1lem  17724  kqreglem1  17726  kqreglem2  17727  kqnrmlem1  17728  kqnrmlem2  17729  reghmph  17778  nrmhmph  17779  opnfbas  17827  rnelfmlem  17937  fmufil  17944  fclscf  18010  fclsfnflim  18012  flimfnfcls  18013  uffclsflim  18016  cnpfcfi  18025  cnpfcf  18026  alexsubALTlem2  18032  alexsubALTlem4  18034  tgpconcompeqg  18094  ghmcnp  18097  divstgplem  18103  tsmsxp  18137  blssps  18407  blss  18408  blcld  18488  metequiv2  18493  met2ndci  18505  prdsxmslem2  18512  txmetcnp  18530  nlmvscnlem1  18675  xrge0tsms  18818  ipcnlem1  19152  iscmet3  19199  cmetss  19220  minveclem3  19283  pmltpc  19300  ovolscalem2  19363  ovolicc2lem5  19370  ovolicc2  19371  nulmbl2  19384  ioombl1  19409  uniioombllem6  19433  uniioombl  19434  vitalilem3  19455  i1faddlem  19538  mbfmullem  19570  itg2split  19594  lhop2  19852  dvfsumrlim  19868  itgsubst  19886  evlslem1  19889  plydivex  20167  plyexmo  20183  ulmbdd  20267  cxploglim  20769  dchrptlem2  21002  lgsquad2lem2  21096  2sqlem5  21105  dchrvmasumif  21150  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lem3  21166  dchrisum0  21167  dchrmusum  21171  dchrvmasum  21172  pntibndlem3  21239  pntlemp  21257  ostth3  21285  cusgrafilem1  21441  ablo4  21828  smcnlem  22146  pjhthmo  22757  mdslmd1lem1  23781  xrge0tsmsd  24176  xpinpreima2  24258  qqhval2  24319  dya2iocnrect  24584  orvcgteel  24678  orvclteel  24683  derangenlem  24810  cnpcon  24870  txpcon  24872  conpcon  24875  pconpi1  24877  iccllyscon  24890  rellyscon  24891  cvmcov2  24915  cvmliftmolem2  24922  cvmliftmo  24924  cvmliftlem15  24938  cvmliftpht  24958  cvmlift3lem2  24960  relexpsucl  25085  relexpcnv  25086  relexpdm  25088  relexprn  25089  relexpadd  25091  relexpindlem  25092  rtrclreclem.trans  25099  rtrclreclem.min  25100  rtrclind  25102  dedekind  25140  prodmo  25215  fprod2dlem  25257  ax5seglem9  25780  ax5seg  25781  axcontlem8  25814  axcontlem12  25818  cgrextend  25846  btwnouttr2  25860  cgrsub  25883  cgrxfr  25893  btwnxfr  25894  colineardim1  25899  btwnconn1lem6  25930  btwnconn1lem13  25937  btwnconn1lem14  25938  btwnconn3  25941  seglecgr12im  25948  segleantisym  25953  outsideofeq  25968  outsidele  25970  lineunray  25985  linethru  25991  mblfinlem2  26144  cnambfre  26154  areacirclem6  26186  comppfsc  26277  neibastop2lem  26279  neibastop2  26280  istotbnd3  26370  sstotbnd  26374  crngm4  26503  diophin  26721  pellexlem3  26784  pellexlem5  26786  pellex  26788  pell14qrmulcl  26816  jm2.19lem3  26952  jm2.25  26960  jm2.27b  26967  lmhmfgsplit  27052  hbtlem2  27196  hbtlem5  27200  issubmd  27251  psgnunilem4  27288  psgneu  27297  fnchoice  27567  stoweidlem17  27633  stoweidlem53  27669  stoweidlem61  27677  2spotiundisj  28165  cvlcvr1  29822  4atlem12  30094  paddasslem10  30311  paddasslem12  30313  paddasslem13  30314  lhpexle3lem  30493  cdlemd4  30683  cdleme0cq  30697  cdlemefs32sn1aw  30896  cdleme43fsv1snlem  30902  cdleme32d  30926  cdleme32f  30928  cdleme40m  30949  cdleme40n  30950  cdleme42keg  30968  cdleme42mgN  30970  cdleme50trn2  31033  cdleme50trn3  31035  cdlemm10N  31601  dihvalcqpre  31718  dihopelvalcpre  31731  dihmeetlem1N  31773  dihjat1lem  31911  mapd0  32148  mapdh9a  32273
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