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  6037  grpridd  6290  mapdom2  7281  domunfican  7382  fofinf1o  7390  finsschain  7416  wemaplem3  7520  oemapvali  7643  iunfictbso  8000  enfin2i  8206  fin1a2s  8299  distrlem4pr  8908  divdivdiv  9720  divsubdiv  9735  lediv12a  9908  xralrple  10796  seqcaopr  11365  leexp2r  11442  hashbclem  11706  rlimresb  12364  summo  12516  fsum2dlem  12559  bezoutlem3  13045  bezoutlem4  13046  qredeu  13112  pcqmul  13232  pcadd  13263  pockthg  13279  ramub1lem2  13400  mreexexlem4d  13877  issubc3  14051  cofucl  14090  setcmon  14247  setcepi  14248  drsdirfi  14400  poslubmo  14578  ghmpreima  15032  gaorber  15090  odcau  15243  pgpssslw  15253  fislw  15264  lsmsubm  15292  efgsfo  15376  pgpfac1  15643  pgpfaclem2  15645  pgpfaclem3  15646  unitgrp  15777  islmodd  15961  lmodprop2d  16011  lsspropd  16098  lbsextlem4  16238  assapropd  16391  ppttop  17076  epttop  17078  restbas  17227  iscnp4  17332  cnpco  17336  nrmsep  17426  regsep2  17445  ordthauslem  17452  1stcfb  17513  2ndcctbss  17523  2ndcdisj  17524  2ndcomap  17526  dis2ndc  17528  1stcelcls  17529  nlly2i  17544  islly2  17552  hausllycmp  17562  lly1stc  17564  1stckgenlem  17590  ptbasin  17614  txcls  17641  ptcnp  17659  txlly  17673  txnlly  17674  txtube  17677  txcmplem1  17678  txcmplem2  17679  xkococnlem  17696  basqtop  17748  regr1lem  17776  kqreglem1  17778  kqreglem2  17779  kqnrmlem1  17780  kqnrmlem2  17781  reghmph  17830  nrmhmph  17831  filuni  17922  rnelfmlem  17989  fmufil  17996  fclscf  18062  fclsfnflim  18064  flimfnfcls  18065  uffclsflim  18068  cnpfcfi  18077  cnpfcf  18078  alexsublem  18080  alexsubALTlem3  18085  tgpconcompeqg  18146  ghmcnp  18149  divstgplem  18155  blssps  18459  blss  18460  blcld  18540  metequiv2  18545  met2ndci  18557  prdsxmslem2  18564  txmetcnp  18582  nlmvscnlem1  18727  xrge0tsms  18870  ipcnlem1  19204  iscmet3  19251  cmetss  19272  minveclem3  19335  pmltpc  19352  ovolscalem2  19415  ovolicc2lem5  19422  ovolicc2  19423  nulmbl2  19436  ioombl1  19461  uniioombllem6  19485  uniioombl  19486  vitalilem3  19507  i1faddlem  19588  mbfmullem  19620  itg2const2  19636  itg2split  19644  lhop2  19904  dvfsumrlim  19920  itgsubst  19938  evlslem1  19941  plydivex  20219  plyexmo  20235  ulmbdd  20319  cxploglim  20821  dchrptlem2  21054  lgsquad2lem2  21148  2sqlem5  21157  dchrvmasumif  21202  rpvmasum2  21211  dchrisum0re  21212  dchrisum0lem3  21218  dchrisum0  21219  dchrmusum  21223  dchrvmasum  21224  pntibndlem3  21291  pntlemp  21309  ostth3  21337  ablo4  21880  smcnlem  22198  pjhthmo  22809  xrge0tsmsd  24228  xpinpreima2  24310  qqhval2  24371  dya2iocnrect  24636  orvcgteel  24730  orvclteel  24735  cnpcon  24922  txpcon  24924  conpcon  24927  pconpi1  24929  iccllyscon  24942  rellyscon  24943  cvmcov2  24967  cvmliftmolem2  24974  cvmliftmo  24976  cvmliftlem15  24990  cvmliftpht  25010  cvmlift3lem2  25012  relexpsucl  25137  relexpcnv  25138  relexpdm  25140  relexprn  25141  relexpadd  25143  relexpindlem  25144  rtrclreclem.min  25152  rtrclind  25154  prodmo  25267  fprod2dlem  25309  ax5seglem9  25881  ax5seg  25882  axcontlem8  25915  axcontlem12  25919  cgrextend  25947  btwnouttr2  25961  btwnexch2  25962  cgrxfr  25994  lineext  26015  btwnconn1lem5  26030  btwnconn1lem13  26038  btwnconn3  26042  segletr  26053  segleantisym  26054  outsideofeq  26069  outsidele  26071  lineunray  26086  mblfinlem3  26257  mblfinlem4  26258  cnambfre  26267  itg2addnclem  26270  areacirclem5  26310  comppfsc  26401  neibastop2lem  26403  neibastop2  26404  istotbnd3  26494  crngm4  26627  mzpmfp  26818  mzpcompact2lem  26822  diophin  26845  pellexlem3  26908  pellex  26912  pell14qrmulcl  26940  jm2.19lem3  27076  jm2.25  27084  jm2.27b  27091  fnwe2lem2  27140  hbtlem2  27319  hbtlem5  27323  psgnunilem4  27411  psgneu  27420  fnchoice  27690  stoweidlem53  27792  stoweidlem61  27800  cshwsdisj  28319  usg2spthonot0  28421  frgranbnb  28484  frgrancvvdeqlemC  28502  cvlcvr1  30211  4atlem12  30483  cdlemb  30665  paddasslem10  30700  paddasslem12  30702  paddasslem13  30703  lhpexle3lem  30882  cdlemd4  31072  cdlemefs32sn1aw  31285  cdleme43fsv1snlem  31291  cdleme32d  31315  cdleme32f  31317  cdleme40m  31338  cdleme40n  31339  cdleme50trn2  31422  cdlemftr3  31436  cdlemm10N  31990  dihvalcqpre  32107  dihopelvalcpre  32120  dihmeetlem1N  32162  dihglblem5apreN  32163  dihmeetlem4preN  32178  dihjat1lem  32300  mapd0  32537  mapdh9a  32662
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