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

Theorem simprrr 741
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simprrr  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  th )

Proof of Theorem simprrr
StepHypRef Expression
1 simpr 447 . 2  |-  ( ( ch  /\  th )  ->  th )
21ad2antll 709 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  fliftfun  5898  grpridd  6147  mapdom2  7120  domunfican  7219  fofinf1o  7227  finsschain  7252  wemaplem3  7353  oemapvali  7476  iunfictbso  7831  enfin2i  8037  fin1a2s  8130  distrlem4pr  8740  divdivdiv  9551  divsubdiv  9566  lediv12a  9739  xralrple  10624  seqcaopr  11175  leexp2r  11252  hashbclem  11486  rlimresb  12135  summo  12287  fsum2dlem  12330  bezoutlem3  12816  bezoutlem4  12817  qredeu  12883  pcqmul  13003  pcadd  13034  pockthg  13050  ramub1lem2  13171  mreexexlem4d  13648  issubc3  13822  cofucl  13861  setcmon  14018  setcepi  14019  drsdirfi  14171  poslubmo  14349  ghmpreima  14803  gaorber  14861  odcau  15014  pgpssslw  15024  fislw  15035  lsmsubm  15063  efgsfo  15147  pgpfac1  15414  pgpfaclem2  15416  pgpfaclem3  15417  unitgrp  15548  islmodd  15732  lmodprop2d  15786  lsspropd  15873  lbsextlem4  16013  assapropd  16166  ppttop  16850  epttop  16852  restbas  16995  cnpco  17102  nrmsep  17191  regsep2  17210  ordthauslem  17217  1stcfb  17277  2ndcctbss  17287  2ndcdisj  17288  2ndcomap  17290  dis2ndc  17292  1stcelcls  17293  nlly2i  17308  islly2  17316  hausllycmp  17326  lly1stc  17328  1stckgenlem  17354  ptbasin  17378  txcls  17405  ptcnp  17422  txlly  17436  txnlly  17437  txtube  17440  txcmplem1  17441  txcmplem2  17442  xkococnlem  17459  basqtop  17508  regr1lem  17536  kqreglem1  17538  kqreglem2  17539  kqnrmlem1  17540  kqnrmlem2  17541  reghmph  17590  nrmhmph  17591  filuni  17682  rnelfmlem  17749  fmufil  17756  fclscf  17822  fclsfnflim  17824  flimfnfcls  17825  uffclsflim  17828  cnpfcfi  17837  cnpfcf  17838  alexsublem  17840  alexsubALTlem3  17845  tgpconcompeqg  17896  ghmcnp  17899  divstgplem  17905  blss  18074  blcld  18153  metequiv2  18158  met2ndci  18170  prdsxmslem2  18177  txmetcnp  18195  nlmvscnlem1  18299  xrge0tsms  18442  ipcnlem1  18776  iscmet3  18823  cmetss  18844  minveclem3  18897  pmltpc  18914  ovolscalem2  18977  ovolicc2lem5  18984  ovolicc2  18985  nulmbl2  18998  ioombl1  19023  uniioombllem6  19047  uniioombl  19048  vitalilem3  19069  i1faddlem  19152  mbfmullem  19184  itg2const2  19200  itg2split  19208  lhop2  19466  dvfsumrlim  19482  itgsubst  19500  evlslem1  19503  plydivex  19781  plyexmo  19797  ulmbdd  19881  cxploglim  20383  dchrptlem2  20616  lgsquad2lem2  20710  2sqlem5  20719  dchrvmasumif  20764  rpvmasum2  20773  dchrisum0re  20774  dchrisum0lem3  20780  dchrisum0  20781  dchrmusum  20785  dchrvmasum  20786  pntibndlem3  20853  pntlemp  20871  ostth3  20899  ablo4  21066  smcnlem  21384  pjhthmo  21995  xrge0tsmsd  23415  iscnp4  23447  xpinpreima2  23461  qqhval2  23639  dya2iocnrect  23895  orvcgteel  23974  orvclteel  23979  cnpcon  24165  txpcon  24167  conpcon  24170  pconpi1  24172  iccllyscon  24185  rellyscon  24186  cvmcov2  24210  cvmliftmolem2  24217  cvmliftmo  24219  cvmliftlem15  24233  cvmliftpht  24253  cvmlift3lem2  24255  relexpsucl  24432  relexpcnv  24433  relexpdm  24436  relexprn  24437  relexpadd  24439  relexpindlem  24440  rtrclreclem.min  24448  rtrclind  24450  prodmo  24563  ax5seglem9  25124  ax5seg  25125  axcontlem8  25158  axcontlem12  25162  cgrextend  25190  btwnouttr2  25204  btwnexch2  25205  cgrxfr  25237  lineext  25258  btwnconn1lem5  25273  btwnconn1lem13  25281  btwnconn3  25285  segletr  25296  segleantisym  25297  outsideofeq  25312  outsidele  25314  lineunray  25329  itg2addnclem  25492  itg2addnc  25494  areacirclem6  25522  comppfsc  25631  neibastop2lem  25633  neibastop2  25634  istotbnd3  25818  crngm4  25951  mzpmfp  26148  mzpcompact2lem  26152  diophin  26175  pellexlem3  26239  pellex  26243  pell14qrmulcl  26271  jm2.19lem3  26407  jm2.25  26415  jm2.27b  26422  fnwe2lem2  26471  hbtlem2  26651  hbtlem5  26655  psgnunilem4  26743  psgneu  26752  fnchoice  27023  stoweidlem53  27125  frgrancvvdeqlemC  27872  cvlcvr1  29598  4atlem12  29870  cdlemb  30052  paddasslem10  30087  paddasslem12  30089  paddasslem13  30090  lhpexle3lem  30269  cdlemd4  30459  cdlemefs32sn1aw  30672  cdleme43fsv1snlem  30678  cdleme32d  30702  cdleme32f  30704  cdleme40m  30725  cdleme40n  30726  cdleme50trn2  30809  cdlemftr3  30823  cdlemm10N  31377  dihvalcqpre  31494  dihopelvalcpre  31507  dihmeetlem1N  31549  dihglblem5apreN  31550  dihmeetlem4preN  31565  dihjat1lem  31687  mapd0  31924  mapdh9a  32049
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