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

Theorem simprrl 765
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 457 . 2  |-  ( ( ch  /\  th )  ->  ch )
21ad2antll 728 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  grpridd  6500  eroveu  7408  undom  7607  mapdom2  7690  domunfican  7795  fofinf1o  7803  finsschain  7829  wemaplem3  7976  oemapvali  8106  iunfictbso  8498  enfin2i  8704  fin1a2s  8797  ttukeylem6  8897  distrlem4pr  9407  mulcmpblnr  9451  prsrlem1  9452  dedekind  9747  divdivdiv  10251  divmuleq  10255  divsubdiv  10266  lediv12a  10444  xralrple  11413  ssfzo12bi  11886  seqcaopr  12123  leexp2r  12202  hashbclem  12480  wrd2ind  12682  rlimresb  13367  summo  13518  fsum2dlem  13564  bezoutlem3  14055  bezoutlem4  14056  qredeu  14125  pcqmul  14254  pcadd  14285  pockthg  14301  prmreclem2  14312  vdwlem10  14385  ramub1lem2  14422  cshwsdisj  14460  mreexexlem4d  14921  mreexdomd  14923  issubc3  15092  cofucl  15131  setcmon  15288  setcepi  15289  drsdirfi  15441  poslubmo  15650  posglbmo  15651  issubmd  15854  mrcmndind  15871  ghmpreima  16162  gaorber  16220  psgnunilem4  16396  psgneu  16405  odcau  16498  pgpssslw  16508  fislw  16519  lsmsubm  16547  efgsfo  16631  gsum2d2  16876  pgpfac1lem5  17004  pgpfac1  17005  pgpfaclem2  17007  pgpfaclem3  17008  unitgrp  17190  lmodprop2d  17446  lsspropd  17537  lbsextlem4  17681  assapropd  17850  evlslem1  18058  mdetunilem8  18994  mdetuni0  18996  mdetmul  18998  neiint  19478  restbas  19532  iscnp4  19637  cnpco  19641  nrmsep  19731  regsep2  19750  ordthauslem  19757  1stcfb  19819  1stcrest  19827  2ndcctbss  19829  2ndcdisj  19830  2ndcomap  19832  dis2ndc  19834  nlly2i  19850  islly2  19858  hausllycmp  19868  lly1stc  19870  comppfsc  19906  ptbasin  19951  txcls  19978  ptcnp  19996  txlly  20010  txnlly  20011  txtube  20014  txcmplem1  20015  txcmplem2  20016  xkococnlem  20033  basqtop  20085  regr1lem  20113  kqreglem1  20115  kqreglem2  20116  kqnrmlem1  20117  kqnrmlem2  20118  reghmph  20167  nrmhmph  20168  opnfbas  20216  rnelfmlem  20326  fmufil  20333  fclscf  20399  fclsfnflim  20401  flimfnfcls  20402  uffclsflim  20405  cnpfcfi  20414  cnpfcf  20415  alexsubALTlem2  20421  alexsubALTlem4  20423  tgpconcompeqg  20483  ghmcnp  20486  qustgplem  20492  tsmsxp  20530  blssps  20800  blss  20801  blcld  20881  metequiv2  20886  met2ndci  20898  prdsxmslem2  20905  txmetcnp  20923  nlmvscnlem1  21068  xrge0tsms  21212  ipcnlem1  21558  iscmet3  21605  cmetss  21626  minveclem3  21717  pmltpc  21735  ovolscalem2  21798  ovolicc2lem5  21805  ovolicc2  21806  nulmbl2  21820  ioombl1  21845  uniioombllem6  21870  uniioombl  21871  vitalilem3  21892  i1faddlem  21973  mbfmullem  22005  itg2split  22029  lhop2  22289  dvfsumrlim  22305  itgsubst  22323  plydivex  22565  plyexmo  22581  ulmbdd  22665  cxploglim  23179  dchrptlem2  23412  lgsquad2lem2  23506  2sqlem5  23515  dchrvmasumif  23560  rpvmasum2  23569  dchrisum0re  23570  dchrisum0lem3  23576  dchrisum0  23577  dchrmusum  23581  dchrvmasum  23582  pntibndlem3  23649  pntlemp  23667  ostth3  23695  legtrid  23850  mirreu3  23907  midexlem  23941  opphllem  23981  mideulem  23982  opphllem1  23991  ax5seglem9  24112  ax5seg  24113  axcontlem8  24146  axcontlem12  24150  cusgrafilem1  24351  2spotiundisj  24934  ablo4  25161  smcnlem  25479  pjhthmo  26092  mdslmd1lem1  27116  xrge0tsmsd  27648  locfinref  27717  xpinpreima2  27762  qqhval2  27836  dya2iocnrect  28125  orvcgteel  28279  orvclteel  28284  derangenlem  28488  cnpcon  28548  txpcon  28550  conpcon  28553  pconpi1  28555  iccllyscon  28568  rellyscon  28569  cvmcov2  28593  cvmliftmolem2  28600  cvmliftmo  28602  cvmliftlem15  28616  cvmliftpht  28636  cvmlift3lem2  28638  relexpsucl  28928  relexpcnv  28929  relexpdm  28931  relexprn  28932  relexpadd  28934  relexpindlem  28935  rtrclreclem.trans  28942  rtrclreclem.min  28943  rtrclind  28945  prodmo  29043  fprod2dlem  29085  cgrextend  29633  btwnouttr2  29647  cgrsub  29670  cgrxfr  29680  btwnxfr  29681  colineardim1  29686  btwnconn1lem6  29717  btwnconn1lem13  29724  btwnconn1lem14  29725  btwnconn3  29728  seglecgr12im  29735  segleantisym  29740  outsideofeq  29755  outsidele  29757  lineunray  29772  linethru  29778  mblfinlem3  30028  cnambfre  30038  areacirclem5  30086  fnessref  30150  neibastop2lem  30153  neibastop2  30154  istotbnd3  30242  sstotbnd  30246  crngm4  30375  diophin  30681  pellexlem3  30742  pellexlem5  30744  pellex  30746  pell14qrmulcl  30774  jm2.19lem3  30908  jm2.25  30916  jm2.27b  30923  lmhmfgsplit  31007  hbtlem2  31048  hbtlem5  31052  fnchoice  31358  stoweidlem17  31688  stoweidlem53  31724  stoweidlem61  31732  rabsubmgmd  32317  lindslinindsimp1  32793  bj-finsumval0  34403  cvlcvr1  34804  4atlem12  35076  paddasslem10  35293  paddasslem12  35295  paddasslem13  35296  lhpexle3lem  35475  cdlemd4  35666  cdleme0cq  35680  cdlemefs32sn1aw  35880  cdleme43fsv1snlem  35886  cdleme32d  35910  cdleme32f  35912  cdleme40m  35933  cdleme40n  35934  cdleme42keg  35952  cdleme42mgN  35954  cdleme50trn2  36017  cdleme50trn3  36019  cdlemm10N  36585  dihvalcqpre  36702  dihopelvalcpre  36715  dihmeetlem1N  36757  dihjat1lem  36895  mapd0  37132  mapdh9a  37257
  Copyright terms: Public domain W3C validator