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

Theorem simprrl 763
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  6306  eroveu  7198  undom  7402  mapdom2  7485  domunfican  7587  fofinf1o  7595  finsschain  7621  wemaplem3  7765  oemapvali  7895  iunfictbso  8287  enfin2i  8493  fin1a2s  8586  ttukeylem6  8686  distrlem4pr  9198  dedekind  9536  divdivdiv  10035  divmuleq  10039  divsubdiv  10050  lediv12a  10228  xralrple  11178  ssfzo12bi  11625  seqcaopr  11846  leexp2r  11924  hashbclem  12208  wrd2ind  12375  rlimresb  13046  summo  13197  fsum2dlem  13240  bezoutlem3  13727  bezoutlem4  13728  qredeu  13796  pcqmul  13923  pcadd  13954  pockthg  13970  prmreclem2  13981  vdwlem10  14054  ramub1lem2  14091  cshwsdisj  14128  mreexexlem4d  14588  mreexdomd  14590  issubc3  14762  cofucl  14801  setcmon  14958  setcepi  14959  drsdirfi  15111  poslubmo  15319  posglbmo  15320  issubmd  15480  mrcmndind  15497  ghmpreima  15771  gaorber  15829  psgnunilem4  16006  psgneu  16015  odcau  16106  pgpssslw  16116  fislw  16127  lsmsubm  16155  efgsfo  16239  gsum2d2  16469  pgpfac1lem5  16583  pgpfac1  16584  pgpfaclem2  16586  pgpfaclem3  16587  unitgrp  16762  lmodprop2d  17010  lsspropd  17101  lbsextlem4  17245  assapropd  17401  evlslem1  17604  mdetunilem8  18428  mdetuni0  18430  mdetmul  18432  neiint  18711  restbas  18765  iscnp4  18870  cnpco  18874  nrmsep  18964  regsep2  18983  ordthauslem  18990  1stcfb  19052  1stcrest  19060  2ndcctbss  19062  2ndcdisj  19063  2ndcomap  19065  dis2ndc  19067  nlly2i  19083  islly2  19091  hausllycmp  19101  lly1stc  19103  ptbasin  19153  txcls  19180  ptcnp  19198  txlly  19212  txnlly  19213  txtube  19216  txcmplem1  19217  txcmplem2  19218  xkococnlem  19235  basqtop  19287  regr1lem  19315  kqreglem1  19317  kqreglem2  19318  kqnrmlem1  19319  kqnrmlem2  19320  reghmph  19369  nrmhmph  19370  opnfbas  19418  rnelfmlem  19528  fmufil  19535  fclscf  19601  fclsfnflim  19603  flimfnfcls  19604  uffclsflim  19607  cnpfcfi  19616  cnpfcf  19617  alexsubALTlem2  19623  alexsubALTlem4  19625  tgpconcompeqg  19685  ghmcnp  19688  divstgplem  19694  tsmsxp  19732  blssps  20002  blss  20003  blcld  20083  metequiv2  20088  met2ndci  20100  prdsxmslem2  20107  txmetcnp  20125  nlmvscnlem1  20270  xrge0tsms  20414  ipcnlem1  20760  iscmet3  20807  cmetss  20828  minveclem3  20919  pmltpc  20937  ovolscalem2  21000  ovolicc2lem5  21007  ovolicc2  21008  nulmbl2  21021  ioombl1  21046  uniioombllem6  21071  uniioombl  21072  vitalilem3  21093  i1faddlem  21174  mbfmullem  21206  itg2split  21230  lhop2  21490  dvfsumrlim  21506  itgsubst  21524  plydivex  21766  plyexmo  21782  ulmbdd  21866  cxploglim  22374  dchrptlem2  22607  lgsquad2lem2  22701  2sqlem5  22710  dchrvmasumif  22755  rpvmasum2  22764  dchrisum0re  22765  dchrisum0lem3  22771  dchrisum0  22772  dchrmusum  22776  dchrvmasum  22777  pntibndlem3  22844  pntlemp  22862  ostth3  22890  legtrid  23025  mirreu3  23061  midexlem  23089  ax5seglem9  23186  ax5seg  23187  axcontlem8  23220  axcontlem12  23224  cusgrafilem1  23390  ablo4  23777  smcnlem  24095  pjhthmo  24708  mdslmd1lem1  25732  xrge0tsmsd  26256  xpinpreima2  26340  qqhval2  26414  dya2iocnrect  26699  orvcgteel  26853  orvclteel  26858  derangenlem  27062  cnpcon  27122  txpcon  27124  conpcon  27127  pconpi1  27129  iccllyscon  27142  rellyscon  27143  cvmcov2  27167  cvmliftmolem2  27174  cvmliftmo  27176  cvmliftlem15  27190  cvmliftpht  27210  cvmlift3lem2  27212  relexpsucl  27337  relexpcnv  27338  relexpdm  27340  relexprn  27341  relexpadd  27343  relexpindlem  27344  rtrclreclem.trans  27351  rtrclreclem.min  27352  rtrclind  27354  prodmo  27452  fprod2dlem  27494  cgrextend  28042  btwnouttr2  28056  cgrsub  28079  cgrxfr  28089  btwnxfr  28090  colineardim1  28095  btwnconn1lem6  28126  btwnconn1lem13  28133  btwnconn1lem14  28134  btwnconn3  28137  seglecgr12im  28144  segleantisym  28149  outsideofeq  28164  outsidele  28166  lineunray  28181  linethru  28187  mblfinlem3  28433  cnambfre  28443  areacirclem5  28491  comppfsc  28582  neibastop2lem  28584  neibastop2  28585  istotbnd3  28673  sstotbnd  28677  crngm4  28806  diophin  29114  pellexlem3  29175  pellexlem5  29177  pellex  29179  pell14qrmulcl  29207  jm2.19lem3  29343  jm2.25  29351  jm2.27b  29358  lmhmfgsplit  29442  hbtlem2  29483  hbtlem5  29487  fnchoice  29754  stoweidlem17  29815  stoweidlem53  29851  stoweidlem61  29859  2spotiundisj  30658  lindslinindsimp1  30994  bj-finsumval0  32586  cvlcvr1  32987  4atlem12  33259  paddasslem10  33476  paddasslem12  33478  paddasslem13  33479  lhpexle3lem  33658  cdlemd4  33848  cdleme0cq  33862  cdlemefs32sn1aw  34061  cdleme43fsv1snlem  34067  cdleme32d  34091  cdleme32f  34093  cdleme40m  34114  cdleme40n  34115  cdleme42keg  34133  cdleme42mgN  34135  cdleme50trn2  34198  cdleme50trn3  34200  cdlemm10N  34766  dihvalcqpre  34883  dihopelvalcpre  34896  dihmeetlem1N  34938  dihjat1lem  35076  mapd0  35313  mapdh9a  35438
  Copyright terms: Public domain W3C validator