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

Theorem simprrr 743
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 449 . 2  |-  ( ( ch  /\  th )  ->  th )
21ad2antll 711 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  fliftfun  6063  grpridd  6316  mapdom2  7307  domunfican  7408  fofinf1o  7416  finsschain  7442  wemaplem3  7546  oemapvali  7669  iunfictbso  8026  enfin2i  8232  fin1a2s  8325  distrlem4pr  8934  divdivdiv  9746  divsubdiv  9761  lediv12a  9934  xralrple  10822  seqcaopr  11391  leexp2r  11468  hashbclem  11732  rlimresb  12390  summo  12542  fsum2dlem  12585  bezoutlem3  13071  bezoutlem4  13072  qredeu  13138  pcqmul  13258  pcadd  13289  pockthg  13305  ramub1lem2  13426  mreexexlem4d  13903  issubc3  14077  cofucl  14116  setcmon  14273  setcepi  14274  drsdirfi  14426  poslubmo  14604  ghmpreima  15058  gaorber  15116  odcau  15269  pgpssslw  15279  fislw  15290  lsmsubm  15318  efgsfo  15402  pgpfac1  15669  pgpfaclem2  15671  pgpfaclem3  15672  unitgrp  15803  islmodd  15987  lmodprop2d  16037  lsspropd  16124  lbsextlem4  16264  assapropd  16417  ppttop  17102  epttop  17104  restbas  17253  iscnp4  17358  cnpco  17362  nrmsep  17452  regsep2  17471  ordthauslem  17478  1stcfb  17539  2ndcctbss  17549  2ndcdisj  17550  2ndcomap  17552  dis2ndc  17554  1stcelcls  17555  nlly2i  17570  islly2  17578  hausllycmp  17588  lly1stc  17590  1stckgenlem  17616  ptbasin  17640  txcls  17667  ptcnp  17685  txlly  17699  txnlly  17700  txtube  17703  txcmplem1  17704  txcmplem2  17705  xkococnlem  17722  basqtop  17774  regr1lem  17802  kqreglem1  17804  kqreglem2  17805  kqnrmlem1  17806  kqnrmlem2  17807  reghmph  17856  nrmhmph  17857  filuni  17948  rnelfmlem  18015  fmufil  18022  fclscf  18088  fclsfnflim  18090  flimfnfcls  18091  uffclsflim  18094  cnpfcfi  18103  cnpfcf  18104  alexsublem  18106  alexsubALTlem3  18111  tgpconcompeqg  18172  ghmcnp  18175  divstgplem  18181  blssps  18485  blss  18486  blcld  18566  metequiv2  18571  met2ndci  18583  prdsxmslem2  18590  txmetcnp  18608  nlmvscnlem1  18753  xrge0tsms  18896  ipcnlem1  19230  iscmet3  19277  cmetss  19298  minveclem3  19361  pmltpc  19378  ovolscalem2  19441  ovolicc2lem5  19448  ovolicc2  19449  nulmbl2  19462  ioombl1  19487  uniioombllem6  19511  uniioombl  19512  vitalilem3  19533  i1faddlem  19614  mbfmullem  19646  itg2const2  19662  itg2split  19670  lhop2  19930  dvfsumrlim  19946  itgsubst  19964  evlslem1  19967  plydivex  20245  plyexmo  20261  ulmbdd  20345  cxploglim  20847  dchrptlem2  21080  lgsquad2lem2  21174  2sqlem5  21183  dchrvmasumif  21228  rpvmasum2  21237  dchrisum0re  21238  dchrisum0lem3  21244  dchrisum0  21245  dchrmusum  21249  dchrvmasum  21250  pntibndlem3  21317  pntlemp  21335  ostth3  21363  ablo4  21906  smcnlem  22224  pjhthmo  22835  xrge0tsmsd  24254  xpinpreima2  24336  qqhval2  24397  dya2iocnrect  24662  orvcgteel  24756  orvclteel  24761  cnpcon  24948  txpcon  24950  conpcon  24953  pconpi1  24955  iccllyscon  24968  rellyscon  24969  cvmcov2  24993  cvmliftmolem2  25000  cvmliftmo  25002  cvmliftlem15  25016  cvmliftpht  25036  cvmlift3lem2  25038  relexpsucl  25163  relexpcnv  25164  relexpdm  25166  relexprn  25167  relexpadd  25169  relexpindlem  25170  rtrclreclem.min  25178  rtrclind  25180  prodmo  25293  fprod2dlem  25335  ax5seglem9  25907  ax5seg  25908  axcontlem8  25941  axcontlem12  25945  cgrextend  25973  btwnouttr2  25987  btwnexch2  25988  cgrxfr  26020  lineext  26041  btwnconn1lem5  26056  btwnconn1lem13  26064  btwnconn3  26068  segletr  26079  segleantisym  26080  outsideofeq  26095  outsidele  26097  lineunray  26112  mblfinlem3  26281  mblfinlem4  26282  cnambfre  26291  itg2addnclem  26294  areacirclem5  26334  comppfsc  26425  neibastop2lem  26427  neibastop2  26428  istotbnd3  26518  crngm4  26651  mzpmfp  26842  mzpcompact2lem  26846  diophin  26869  pellexlem3  26932  pellex  26936  pell14qrmulcl  26964  jm2.19lem3  27100  jm2.25  27108  jm2.27b  27115  fnwe2lem2  27164  hbtlem2  27343  hbtlem5  27347  psgnunilem4  27435  psgneu  27444  fnchoice  27714  stoweidlem53  27816  stoweidlem61  27824  cshwsdisj  28343  usg2spthonot0  28445  frgranbnb  28508  frgrancvvdeqlemC  28526  cvlcvr1  30235  4atlem12  30507  cdlemb  30689  paddasslem10  30724  paddasslem12  30726  paddasslem13  30727  lhpexle3lem  30906  cdlemd4  31096  cdlemefs32sn1aw  31309  cdleme43fsv1snlem  31315  cdleme32d  31339  cdleme32f  31341  cdleme40m  31362  cdleme40n  31363  cdleme50trn2  31446  cdlemftr3  31460  cdlemm10N  32014  dihvalcqpre  32131  dihopelvalcpre  32144  dihmeetlem1N  32186  dihglblem5apreN  32187  dihmeetlem4preN  32202  dihjat1lem  32324  mapd0  32561  mapdh9a  32686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator