Theorem simprrl 804

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

Step	Hyp	Ref	Expression
1		simpl 473	. 2 |- ( ( ch /\ th ) -> ch )
2	1	ad2antll 765	1 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  prproe  4434  f1prex  6539  grpridd  6874  wfrlem17  7431  eroveu  7842  undom  8048  mapdom2  8131  domunfican  8233  fofinf1o  8241  finsschain  8273  wemaplem3  8453  oemapvali  8581  iunfictbso  8937  enfin2i  9143  fin1a2s  9236  ttukeylem6  9336  distrlem4pr  9848  mulcmpblnr  9892  prsrlem1  9893  dedekind  10200  divdivdiv  10726  divmuleq  10730  divsubdiv  10741  lediv12a  10916  xralrple  12036  ssfzo12bi  12563  seqcaopr  12838  leexp2r  12918  hashbclem  13236  wrd2ind  13477  rtrclreclem3  13800  rtrclreclem4  13801  relexpindlem  13803  rtrclind  13805  rlimresb  14296  summo  14448  fsum2dlem  14501  prodmo  14666  fprod2dlem  14710  bezoutlem3  15258  bezoutlem4  15259  ncoprmgcdne1b  15363  qredeu  15372  coprmproddvdslem  15376  pcqmul  15558  pcadd  15593  pockthg  15610  prmreclem2  15621  vdwlem10  15694  ramub1lem2  15731  prmgaplem6  15760  prmgaplem7  15761  cshwsdisj  15805  mreexexlem4d  16307  mreexdomd  16310  issubc3  16509  cofucl  16548  setcmon  16737  setcepi  16738  drsdirfi  16938  poslubmo  17146  posglbmo  17147  issubmd  17349  mrcmndind  17366  ghmpreima  17682  gaorber  17741  psgnunilem4  17917  psgneu  17926  odcau  18019  pgpssslw  18029  fislw  18040  lsmsubm  18068  efgsfo  18152  gsum2d2  18373  pgpfac1lem5  18478  pgpfac1  18479  pgpfaclem2  18481  pgpfaclem3  18482  unitgrp  18667  lmodprop2d  18925  lsspropd  19017  lbsextlem4  19161  assapropd  19327  evlslem1  19515  mdetunilem8  20425  mdetuni0  20427  mdetmul  20429  neiint  20908  restbas  20962  iscnp4  21067  cnpco  21071  nrmsep  21161  regsep2  21180  ordthauslem  21187  1stcfb  21248  1stcrest  21256  2ndcctbss  21258  2ndcdisj  21259  2ndcomap  21261  dis2ndc  21263  nlly2i  21279  islly2  21287  hausllycmp  21297  lly1stc  21299  comppfsc  21335  ptbasin  21380  txcls  21407  ptcnp  21425  txlly  21439  txnlly  21440  txtube  21443  txcmplem1  21444  txcmplem2  21445  xkococnlem  21462  basqtop  21514  regr1lem  21542  kqreglem1  21544  kqreglem2  21545  kqnrmlem1  21546  kqnrmlem2  21547  reghmph  21596  nrmhmph  21597  opnfbas  21646  rnelfmlem  21756  fmufil  21763  fclscf  21829  fclsfnflim  21831  flimfnfcls  21832  uffclsflim  21835  cnpfcfi  21844  cnpfcf  21845  alexsubALTlem2  21852  alexsubALTlem4  21854  tgpconncompeqg  21915  ghmcnp  21918  qustgplem  21924  tsmsxp  21958  blssps  22229  blss  22230  blcld  22310  metequiv2  22315  met2ndci  22327  prdsxmslem2  22334  txmetcnp  22352  nlmvscnlem1  22490  xrge0tsms  22637  ipcnlem1  23044  iscmet3  23091  cmetss  23113  minveclem3  23200  pmltpc  23219  ovolscalem2  23282  ovolicc2lem5  23289  ovolicc2  23290  nulmbl2  23304  ioombl1  23330  uniioombllem6  23356  uniioombl  23357  vitalilem3  23379  i1faddlem  23460  mbfmullem  23492  itg2split  23516  lhop2  23778  dvfsumrlim  23794  itgsubst  23812  plydivex  24052  plyexmo  24068  ulmbdd  24152  cxploglim  24704  dchrptlem2  24990  lgsquad2lem2  25110  2sqlem5  25147  dchrvmasumif  25192  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lem3  25208  dchrisum0  25209  dchrmusum  25213  dchrvmasum  25214  pntibndlem3  25281  pntlemp  25299  ostth3  25327  legtrid  25486  hlcgreu  25513  mirreu3  25549  midexlem  25587  opphllem  25627  mideulem  25628  opphllem1  25639  oppperpex  25645  lnperpex  25695  trgcopy  25696  iscgra1  25702  cgraswap  25712  cgracom  25714  cgratr  25715  acopyeu  25725  ax5seglem9  25817  ax5seg  25818  axcontlem8  25851  axcontlem12  25855  2pthfrgr  27148  frgrnbnb  27157  ablo4  27404  smcnlem  27552  pjhthmo  28161  mdslmd1lem1  29184  xrge0tsmsd  29785  locfinref  29908  xpinpreima2  29953  qqhval2  30026  dya2iocnrect  30343  orvcgteel  30529  orvclteel  30534  derangenlem  31153  cnpconn  31212  txpconn  31214  connpconn  31217  pconnpi1  31219  iccllysconn  31232  rellysconn  31233  cvmcov2  31257  cvmliftmolem2  31264  cvmliftmo  31266  cvmliftlem15  31280  cvmliftpht  31300  cvmlift3lem2  31302  nosupbnd1lem1  31854  nosupbnd2  31862  conway  31910  cgrextend  32115  btwnouttr2  32129  cgrsub  32152  cgrxfr  32162  btwnxfr  32163  colineardim1  32168  btwnconn1lem6  32199  btwnconn1lem13  32206  btwnconn1lem14  32207  btwnconn3  32210  seglecgr12im  32217  segleantisym  32222  outsideofeq  32237  outsidele  32239  lineunray  32254  linethru  32260  fnessref  32352  neibastop2lem  32355  neibastop2  32356  unblimceq0lem  32497  knoppndvlem22  32524  bj-finsumval0  33147  isbasisrelowllem1  33203  isbasisrelowllem2  33204  mblfinlem3  33448  cnambfre  33458  areacirclem5  33504  istotbnd3  33570  sstotbnd  33574  crngm4  33802  cvlcvr1  34626  4atlem12  34898  paddasslem10  35115  paddasslem12  35117  paddasslem13  35118  lhpexle3lem  35297  cdlemd4  35488  cdleme0cq  35502  cdlemefs32sn1aw  35702  cdleme43fsv1snlem  35708  cdleme32d  35732  cdleme32f  35734  cdleme40m  35755  cdleme40n  35756  cdleme42keg  35774  cdleme42mgN  35776  cdleme50trn2  35839  cdleme50trn3  35841  cdlemm10N  36407  dihvalcqpre  36524  dihopelvalcpre  36537  dihmeetlem1N  36579  dihjat1lem  36717  mapd0  36954  mapdh9a  37079  diophin  37336  pellexlem3  37395  pellexlem5  37397  pellex  37399  pell14qrmulcl  37427  jm2.19lem3  37558  jm2.25  37566  jm2.27b  37573  lmhmfgsplit  37656  hbtlem2  37694  hbtlem5  37698  gsumws3  38499  gsumws4  38500  fnchoice  39188  stoweidlem17  40234  stoweidlem53  40270  stoweidlem61  40278  qndenserrnbllem  40514  bgoldbtbnd  41697  rabsubmgmd  41791  lindslinindsimp1  42246