Theorem simprrr 742

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

Step	Hyp	Ref	Expression
1		simpr 448	. 2 |- ( ( ch /\ th ) -> th )
2	1	ad2antll 710	1 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 359

This theorem is referenced by:  fliftfun  5993  grpridd  6246  mapdom2  7237  domunfican  7338  fofinf1o  7346  finsschain  7371  wemaplem3  7473  oemapvali  7596  iunfictbso  7951  enfin2i  8157  fin1a2s  8250  distrlem4pr  8859  divdivdiv  9671  divsubdiv  9686  lediv12a  9859  xralrple  10747  seqcaopr  11315  leexp2r  11392  hashbclem  11656  rlimresb  12314  summo  12466  fsum2dlem  12509  bezoutlem3  12995  bezoutlem4  12996  qredeu  13062  pcqmul  13182  pcadd  13213  pockthg  13229  ramub1lem2  13350  mreexexlem4d  13827  issubc3  14001  cofucl  14040  setcmon  14197  setcepi  14198  drsdirfi  14350  poslubmo  14528  ghmpreima  14982  gaorber  15040  odcau  15193  pgpssslw  15203  fislw  15214  lsmsubm  15242  efgsfo  15326  pgpfac1  15593  pgpfaclem2  15595  pgpfaclem3  15596  unitgrp  15727  islmodd  15911  lmodprop2d  15961  lsspropd  16048  lbsextlem4  16188  assapropd  16341  ppttop  17026  epttop  17028  restbas  17176  iscnp4  17281  cnpco  17285  nrmsep  17375  regsep2  17394  ordthauslem  17401  1stcfb  17461  2ndcctbss  17471  2ndcdisj  17472  2ndcomap  17474  dis2ndc  17476  1stcelcls  17477  nlly2i  17492  islly2  17500  hausllycmp  17510  lly1stc  17512  1stckgenlem  17538  ptbasin  17562  txcls  17589  ptcnp  17607  txlly  17621  txnlly  17622  txtube  17625  txcmplem1  17626  txcmplem2  17627  xkococnlem  17644  basqtop  17696  regr1lem  17724  kqreglem1  17726  kqreglem2  17727  kqnrmlem1  17728  kqnrmlem2  17729  reghmph  17778  nrmhmph  17779  filuni  17870  rnelfmlem  17937  fmufil  17944  fclscf  18010  fclsfnflim  18012  flimfnfcls  18013  uffclsflim  18016  cnpfcfi  18025  cnpfcf  18026  alexsublem  18028  alexsubALTlem3  18033  tgpconcompeqg  18094  ghmcnp  18097  divstgplem  18103  blssps  18407  blss  18408  blcld  18488  metequiv2  18493  met2ndci  18505  prdsxmslem2  18512  txmetcnp  18530  nlmvscnlem1  18675  xrge0tsms  18818  ipcnlem1  19152  iscmet3  19199  cmetss  19220  minveclem3  19283  pmltpc  19300  ovolscalem2  19363  ovolicc2lem5  19370  ovolicc2  19371  nulmbl2  19384  ioombl1  19409  uniioombllem6  19433  uniioombl  19434  vitalilem3  19455  i1faddlem  19538  mbfmullem  19570  itg2const2  19586  itg2split  19594  lhop2  19852  dvfsumrlim  19868  itgsubst  19886  evlslem1  19889  plydivex  20167  plyexmo  20183  ulmbdd  20267  cxploglim  20769  dchrptlem2  21002  lgsquad2lem2  21096  2sqlem5  21105  dchrvmasumif  21150  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lem3  21166  dchrisum0  21167  dchrmusum  21171  dchrvmasum  21172  pntibndlem3  21239  pntlemp  21257  ostth3  21285  ablo4  21828  smcnlem  22146  pjhthmo  22757  xrge0tsmsd  24176  xpinpreima2  24258  qqhval2  24319  dya2iocnrect  24584  orvcgteel  24678  orvclteel  24683  cnpcon  24870  txpcon  24872  conpcon  24875  pconpi1  24877  iccllyscon  24890  rellyscon  24891  cvmcov2  24915  cvmliftmolem2  24922  cvmliftmo  24924  cvmliftlem15  24938  cvmliftpht  24958  cvmlift3lem2  24960  relexpsucl  25085  relexpcnv  25086  relexpdm  25088  relexprn  25089  relexpadd  25091  relexpindlem  25092  rtrclreclem.min  25100  rtrclind  25102  prodmo  25215  fprod2dlem  25257  ax5seglem9  25780  ax5seg  25781  axcontlem8  25814  axcontlem12  25818  cgrextend  25846  btwnouttr2  25860  btwnexch2  25861  cgrxfr  25893  lineext  25914  btwnconn1lem5  25929  btwnconn1lem13  25937  btwnconn3  25941  segletr  25952  segleantisym  25953  outsideofeq  25968  outsidele  25970  lineunray  25985  mblfinlem2  26144  mblfinlem3  26145  cnambfre  26154  itg2addnclem  26155  areacirclem6  26186  comppfsc  26277  neibastop2lem  26279  neibastop2  26280  istotbnd3  26370  crngm4  26503  mzpmfp  26694  mzpcompact2lem  26698  diophin  26721  pellexlem3  26784  pellex  26788  pell14qrmulcl  26816  jm2.19lem3  26952  jm2.25  26960  jm2.27b  26967  fnwe2lem2  27016  hbtlem2  27196  hbtlem5  27200  psgnunilem4  27288  psgneu  27297  fnchoice  27567  stoweidlem53  27669  stoweidlem61  27677  usg2spthonot0  28086  frgranbnb  28124  frgrancvvdeqlemC  28142  cvlcvr1  29822  4atlem12  30094  cdlemb  30276  paddasslem10  30311  paddasslem12  30313  paddasslem13  30314  lhpexle3lem  30493  cdlemd4  30683  cdlemefs32sn1aw  30896  cdleme43fsv1snlem  30902  cdleme32d  30926  cdleme32f  30928  cdleme40m  30949  cdleme40n  30950  cdleme50trn2  31033  cdlemftr3  31047  cdlemm10N  31601  dihvalcqpre  31718  dihopelvalcpre  31731  dihmeetlem1N  31773  dihglblem5apreN  31774  dihmeetlem4preN  31789  dihjat1lem  31911  mapd0  32148  mapdh9a  32273

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361