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  6490  eroveu  7396  undom  7595  mapdom2  7678  domunfican  7782  fofinf1o  7790  finsschain  7816  wemaplem3  7962  oemapvali  8092  iunfictbso  8484  enfin2i  8690  fin1a2s  8783  ttukeylem6  8883  distrlem4pr  9393  mulcmpblnr  9437  prsrlem1  9438  dedekind  9732  divdivdiv  10234  divmuleq  10238  divsubdiv  10249  lediv12a  10427  xralrple  11393  ssfzo12bi  11864  seqcaopr  12100  leexp2r  12178  hashbclem  12454  wrd2ind  12653  rlimresb  13337  summo  13488  fsum2dlem  13534  bezoutlem3  14026  bezoutlem4  14027  qredeu  14096  pcqmul  14225  pcadd  14256  pockthg  14272  prmreclem2  14283  vdwlem10  14356  ramub1lem2  14393  cshwsdisj  14430  mreexexlem4d  14891  mreexdomd  14893  issubc3  15065  cofucl  15104  setcmon  15261  setcepi  15262  drsdirfi  15414  poslubmo  15622  posglbmo  15623  issubmd  15783  mrcmndind  15800  ghmpreima  16076  gaorber  16134  psgnunilem4  16311  psgneu  16320  odcau  16413  pgpssslw  16423  fislw  16434  lsmsubm  16462  efgsfo  16546  gsum2d2  16786  pgpfac1lem5  16913  pgpfac1  16914  pgpfaclem2  16916  pgpfaclem3  16917  unitgrp  17093  lmodprop2d  17348  lsspropd  17439  lbsextlem4  17583  assapropd  17740  evlslem1  17948  mdetunilem8  18881  mdetuni0  18883  mdetmul  18885  neiint  19364  restbas  19418  iscnp4  19523  cnpco  19527  nrmsep  19617  regsep2  19636  ordthauslem  19643  1stcfb  19705  1stcrest  19713  2ndcctbss  19715  2ndcdisj  19716  2ndcomap  19718  dis2ndc  19720  nlly2i  19736  islly2  19744  hausllycmp  19754  lly1stc  19756  ptbasin  19806  txcls  19833  ptcnp  19851  txlly  19865  txnlly  19866  txtube  19869  txcmplem1  19870  txcmplem2  19871  xkococnlem  19888  basqtop  19940  regr1lem  19968  kqreglem1  19970  kqreglem2  19971  kqnrmlem1  19972  kqnrmlem2  19973  reghmph  20022  nrmhmph  20023  opnfbas  20071  rnelfmlem  20181  fmufil  20188  fclscf  20254  fclsfnflim  20256  flimfnfcls  20257  uffclsflim  20260  cnpfcfi  20269  cnpfcf  20270  alexsubALTlem2  20276  alexsubALTlem4  20278  tgpconcompeqg  20338  ghmcnp  20341  divstgplem  20347  tsmsxp  20385  blssps  20655  blss  20656  blcld  20736  metequiv2  20741  met2ndci  20753  prdsxmslem2  20760  txmetcnp  20778  nlmvscnlem1  20923  xrge0tsms  21067  ipcnlem1  21413  iscmet3  21460  cmetss  21481  minveclem3  21572  pmltpc  21590  ovolscalem2  21653  ovolicc2lem5  21660  ovolicc2  21661  nulmbl2  21675  ioombl1  21700  uniioombllem6  21725  uniioombl  21726  vitalilem3  21747  i1faddlem  21828  mbfmullem  21860  itg2split  21884  lhop2  22144  dvfsumrlim  22160  itgsubst  22178  plydivex  22420  plyexmo  22436  ulmbdd  22520  cxploglim  23028  dchrptlem2  23261  lgsquad2lem2  23355  2sqlem5  23364  dchrvmasumif  23409  rpvmasum2  23418  dchrisum0re  23419  dchrisum0lem3  23425  dchrisum0  23426  dchrmusum  23430  dchrvmasum  23431  pntibndlem3  23498  pntlemp  23516  ostth3  23544  legtrid  23698  mirreu3  23741  midexlem  23770  mideulem  23806  ax5seglem9  23909  ax5seg  23910  axcontlem8  23943  axcontlem12  23947  cusgrafilem1  24141  2spotiundisj  24725  ablo4  24951  smcnlem  25269  pjhthmo  25882  mdslmd1lem1  26906  xrge0tsmsd  27424  xpinpreima2  27511  qqhval2  27585  dya2iocnrect  27878  orvcgteel  28032  orvclteel  28037  derangenlem  28241  cnpcon  28301  txpcon  28303  conpcon  28306  pconpi1  28308  iccllyscon  28321  rellyscon  28322  cvmcov2  28346  cvmliftmolem2  28353  cvmliftmo  28355  cvmliftlem15  28369  cvmliftpht  28389  cvmlift3lem2  28391  relexpsucl  28516  relexpcnv  28517  relexpdm  28519  relexprn  28520  relexpadd  28522  relexpindlem  28523  rtrclreclem.trans  28530  rtrclreclem.min  28531  rtrclind  28533  prodmo  28631  fprod2dlem  28673  cgrextend  29221  btwnouttr2  29235  cgrsub  29258  cgrxfr  29268  btwnxfr  29269  colineardim1  29274  btwnconn1lem6  29305  btwnconn1lem13  29312  btwnconn1lem14  29313  btwnconn3  29316  seglecgr12im  29323  segleantisym  29328  outsideofeq  29343  outsidele  29345  lineunray  29360  linethru  29366  mblfinlem3  29617  cnambfre  29627  areacirclem5  29675  comppfsc  29766  neibastop2lem  29768  neibastop2  29769  istotbnd3  29857  sstotbnd  29861  crngm4  29990  diophin  30297  pellexlem3  30358  pellexlem5  30360  pellex  30362  pell14qrmulcl  30390  jm2.19lem3  30526  jm2.25  30534  jm2.27b  30541  lmhmfgsplit  30625  hbtlem2  30666  hbtlem5  30670  fnchoice  30937  stoweidlem17  31272  stoweidlem53  31308  stoweidlem61  31316  lindslinindsimp1  32006  bj-finsumval0  33610  cvlcvr1  34011  4atlem12  34283  paddasslem10  34500  paddasslem12  34502  paddasslem13  34503  lhpexle3lem  34682  cdlemd4  34872  cdleme0cq  34886  cdlemefs32sn1aw  35085  cdleme43fsv1snlem  35091  cdleme32d  35115  cdleme32f  35117  cdleme40m  35138  cdleme40n  35139  cdleme42keg  35157  cdleme42mgN  35159  cdleme50trn2  35222  cdleme50trn3  35224  cdlemm10N  35790  dihvalcqpre  35907  dihopelvalcpre  35920  dihmeetlem1N  35962  dihjat1lem  36100  mapd0  36337  mapdh9a  36462
  Copyright terms: Public domain W3C validator