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

Theorem simprrr 742
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 448 . 2  |-  ( ( ch  /\  th )  ->  th )
21ad2antll 710 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  fliftfun  6025  grpridd  6278  mapdom2  7269  domunfican  7370  fofinf1o  7378  finsschain  7404  wemaplem3  7506  oemapvali  7629  iunfictbso  7984  enfin2i  8190  fin1a2s  8283  distrlem4pr  8892  divdivdiv  9704  divsubdiv  9719  lediv12a  9892  xralrple  10780  seqcaopr  11348  leexp2r  11425  hashbclem  11689  rlimresb  12347  summo  12499  fsum2dlem  12542  bezoutlem3  13028  bezoutlem4  13029  qredeu  13095  pcqmul  13215  pcadd  13246  pockthg  13262  ramub1lem2  13383  mreexexlem4d  13860  issubc3  14034  cofucl  14073  setcmon  14230  setcepi  14231  drsdirfi  14383  poslubmo  14561  ghmpreima  15015  gaorber  15073  odcau  15226  pgpssslw  15236  fislw  15247  lsmsubm  15275  efgsfo  15359  pgpfac1  15626  pgpfaclem2  15628  pgpfaclem3  15629  unitgrp  15760  islmodd  15944  lmodprop2d  15994  lsspropd  16081  lbsextlem4  16221  assapropd  16374  ppttop  17059  epttop  17061  restbas  17210  iscnp4  17315  cnpco  17319  nrmsep  17409  regsep2  17428  ordthauslem  17435  1stcfb  17496  2ndcctbss  17506  2ndcdisj  17507  2ndcomap  17509  dis2ndc  17511  1stcelcls  17512  nlly2i  17527  islly2  17535  hausllycmp  17545  lly1stc  17547  1stckgenlem  17573  ptbasin  17597  txcls  17624  ptcnp  17642  txlly  17656  txnlly  17657  txtube  17660  txcmplem1  17661  txcmplem2  17662  xkococnlem  17679  basqtop  17731  regr1lem  17759  kqreglem1  17761  kqreglem2  17762  kqnrmlem1  17763  kqnrmlem2  17764  reghmph  17813  nrmhmph  17814  filuni  17905  rnelfmlem  17972  fmufil  17979  fclscf  18045  fclsfnflim  18047  flimfnfcls  18048  uffclsflim  18051  cnpfcfi  18060  cnpfcf  18061  alexsublem  18063  alexsubALTlem3  18068  tgpconcompeqg  18129  ghmcnp  18132  divstgplem  18138  blssps  18442  blss  18443  blcld  18523  metequiv2  18528  met2ndci  18540  prdsxmslem2  18547  txmetcnp  18565  nlmvscnlem1  18710  xrge0tsms  18853  ipcnlem1  19187  iscmet3  19234  cmetss  19255  minveclem3  19318  pmltpc  19335  ovolscalem2  19398  ovolicc2lem5  19405  ovolicc2  19406  nulmbl2  19419  ioombl1  19444  uniioombllem6  19468  uniioombl  19469  vitalilem3  19490  i1faddlem  19573  mbfmullem  19605  itg2const2  19621  itg2split  19629  lhop2  19887  dvfsumrlim  19903  itgsubst  19921  evlslem1  19924  plydivex  20202  plyexmo  20218  ulmbdd  20302  cxploglim  20804  dchrptlem2  21037  lgsquad2lem2  21131  2sqlem5  21140  dchrvmasumif  21185  rpvmasum2  21194  dchrisum0re  21195  dchrisum0lem3  21201  dchrisum0  21202  dchrmusum  21206  dchrvmasum  21207  pntibndlem3  21274  pntlemp  21292  ostth3  21320  ablo4  21863  smcnlem  22181  pjhthmo  22792  xrge0tsmsd  24211  xpinpreima2  24293  qqhval2  24354  dya2iocnrect  24619  orvcgteel  24713  orvclteel  24718  cnpcon  24905  txpcon  24907  conpcon  24910  pconpi1  24912  iccllyscon  24925  rellyscon  24926  cvmcov2  24950  cvmliftmolem2  24957  cvmliftmo  24959  cvmliftlem15  24973  cvmliftpht  24993  cvmlift3lem2  24995  relexpsucl  25120  relexpcnv  25121  relexpdm  25123  relexprn  25124  relexpadd  25126  relexpindlem  25127  rtrclreclem.min  25135  rtrclind  25137  prodmo  25251  fprod2dlem  25293  ax5seglem9  25824  ax5seg  25825  axcontlem8  25858  axcontlem12  25862  cgrextend  25890  btwnouttr2  25904  btwnexch2  25905  cgrxfr  25937  lineext  25958  btwnconn1lem5  25973  btwnconn1lem13  25981  btwnconn3  25985  segletr  25996  segleantisym  25997  outsideofeq  26012  outsidele  26014  lineunray  26029  mblfinlem2  26191  mblfinlem3  26192  cnambfre  26201  itg2addnclem  26202  areacirclem6  26233  comppfsc  26324  neibastop2lem  26326  neibastop2  26327  istotbnd3  26417  crngm4  26550  mzpmfp  26741  mzpcompact2lem  26745  diophin  26768  pellexlem3  26831  pellex  26835  pell14qrmulcl  26863  jm2.19lem3  26999  jm2.25  27007  jm2.27b  27014  fnwe2lem2  27063  hbtlem2  27243  hbtlem5  27247  psgnunilem4  27335  psgneu  27344  fnchoice  27614  stoweidlem53  27716  stoweidlem61  27724  shwrdsdisj  28173  usg2spthonot0  28230  frgranbnb  28268  frgrancvvdeqlemC  28286  cvlcvr1  29976  4atlem12  30248  cdlemb  30430  paddasslem10  30465  paddasslem12  30467  paddasslem13  30468  lhpexle3lem  30647  cdlemd4  30837  cdlemefs32sn1aw  31050  cdleme43fsv1snlem  31056  cdleme32d  31080  cdleme32f  31082  cdleme40m  31103  cdleme40n  31104  cdleme50trn2  31187  cdlemftr3  31201  cdlemm10N  31755  dihvalcqpre  31872  dihopelvalcpre  31885  dihmeetlem1N  31927  dihglblem5apreN  31928  dihmeetlem4preN  31943  dihjat1lem  32065  mapd0  32302  mapdh9a  32427
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