Theorem anassrs 680

Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
anassrs.1	|- ( ( ph /\ ( ps /\ ch ) ) -> th )

Assertion

Ref	Expression
anassrs	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Proof of Theorem anassrs

Step	Hyp	Ref	Expression
1		anassrs.1	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
2	1	exp32 631	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp31 448	1 |- ( ( ( ph /\ ps ) /\ ch ) -> th )

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:  anass  681  mpanr1  719  pm2.61ddan  833  pm2.61dda  834  anass1rs  849  anabss5  857  anabss7  862  pm2.61da2ne  2882  ralimdvva  2964  2ralbida  2987  2ralbidva  2988  reximdvva  3019  2rexbidva  3056  copsexg  4956  pofun  5051  imainss  5548  eqfnfv2  6312  fnex  6481  f1elima  6520  fliftfun  6562  isores2  6583  f1oiso  6601  ovmpt2dxf  6786  grpridd  6874  sorpssuni  6946  sorpssint  6947  tfindsg2  7061  oalim  7612  omlim  7613  oaass  7641  omlimcl  7658  omass  7660  oelim2  7675  oeoa  7677  oeoelem  7678  nnaass  7702  omabs  7727  eroveu  7842  sbthlem4  8073  fimaxg  8207  fisupg  8208  fofinf1o  8241  fiming  8404  fiinfg  8405  ordtypelem7  8429  hartogs  8449  card2on  8459  unwdomg  8489  wemapwe  8594  dfac5  8951  cfsmolem  9092  isf32lem2  9176  ttukeylem6  9336  ondomon  9385  alephreg  9404  ltexprlem6  9863  recexsrlem  9924  wloglei  10560  recextlem2  10658  fimaxre  10968  creur  11014  uz11  11710  xrmaxeq  12010  xrmineq  12011  xaddf  12055  xaddass  12079  xleadd1a  12083  xlt2add  12090  xmullem  12094  xmulgt0  12113  xmulasslem3  12116  xlemul1a  12118  xadddilem  12124  fzrevral  12425  seqcaopr2  12837  expnlbnd2  12995  faclbnd4lem4  13083  rtrclreclem3  13800  rtrclreclem4  13801  relexpindlem  13803  rtrclind  13805  shftlem  13808  01sqrex  13990  cau3lem  14094  limsupbnd2  14214  clim2  14235  clim2c  14236  clim0c  14238  rlimresb  14296  2clim  14303  climabs0  14316  climcn1  14322  climcn2  14323  o1rlimmul  14349  climsqz  14371  climsqz2  14372  rlimsqzlem  14379  lo1le  14382  climsup  14400  caucvgrlem2  14405  iseralt  14415  summolem2  14447  fsum2dlem  14501  cvgcmp  14548  cvgcmpce  14550  climfsum  14552  fsumiun  14553  geomulcvg  14607  mertenslem2  14617  mertens  14618  prodfn0  14626  prodfrec  14627  zprod  14667  fprodeq0  14705  fprodn0  14709  fprod2dlem  14710  smu01lem  15207  gcdcllem1  15221  gcdmultiplez  15270  dvdssq  15280  lcmdvds  15321  coprmdvds2  15368  pclem  15543  pcge0  15566  pcgcd1  15581  prmpwdvds  15608  1arithlem4  15630  4sqlem18  15666  vdwlem10  15694  vdwlem11  15695  ramval  15712  ramub1lem2  15731  ramcl  15733  imasaddfnlem  16188  imasaddflem  16190  imasvscafn  16197  imasleval  16201  ismon2  16394  isepi2  16401  issubc3  16509  cofucl  16548  setcmon  16737  setcepi  16738  ipodrsfi  17163  ipodrsima  17165  isacs3lem  17166  grpidpropd  17261  gsumpropd2lem  17273  mhmpropd  17341  mhmima  17363  gsumccat  17378  grplcan  17477  dfgrp3lem  17513  mulgdirlem  17572  subgmulg  17608  issubg4  17613  subgint  17618  cycsubgcl  17620  ssnmz  17636  gastacl  17742  orbsta  17746  cntzsubg  17769  galactghm  17823  odmulg  17973  odbezout  17975  sylow3lem2  18043  lsmsubm  18068  efgsfo  18152  mulgmhm  18233  mulgghm  18234  gsumval3  18308  gsumcllem  18309  gsumpt  18361  gsum2d  18371  gsum2d2  18373  prdsgsum  18377  subgdmdprd  18433  dprd2d2  18443  ablfac1eu  18472  srglmhm  18535  srgrmhm  18536  ringpropd  18582  ringlghm  18604  dvdsrpropd  18696  abvpropd  18842  islmodd  18869  lmodprop2d  18925  lsssubg  18957  lsspropd  19017  lmhmima  19047  lidlsubg  19215  assapropd  19327  asclpropd  19346  psrass1lem  19377  mplcoe1  19465  mplcoe5  19468  mplind  19502  evlslem2  19512  evlsval  19519  coe1tmmul2  19646  phlpropd  20000  frlmsslsp  20135  lindfmm  20166  islindf4  20177  mamuass  20208  mavmulass  20355  mdetuni0  20427  mdetmul  20429  cpmatacl  20521  cpmadugsumfi  20682  cpmadumatpolylem1  20686  cpmadumatpolylem2  20687  cpmadumatpoly  20688  cayhamlem4  20693  neips  20917  neindisj  20921  ordtrest2lem  21007  lmbrf  21064  lmss  21102  isreg2  21181  lmmo  21184  hauscmplem  21209  bwth  21213  2ndcomap  21261  1stcelcls  21264  restlly  21286  islly2  21287  cldllycmp  21298  comppfsc  21335  1stckgenlem  21356  txbas  21370  txbasval  21409  tx1cn  21412  ptpjopn  21415  ptcnp  21425  txnlly  21440  txlm  21451  xkococn  21463  fgabs  21683  fmfnfmlem4  21761  flimcf  21786  hauspwpwf1  21791  fclsbas  21825  fclscf  21829  flimfnfcls  21832  ghmcnp  21918  tsmsxp  21958  isxmet2d  22132  elmopn2  22250  mopni3  22299  blsscls2  22309  metequiv2  22315  metss2lem  22316  met2ndci  22327  metrest  22329  metcnp  22346  metcnp2  22347  metcnpi3  22351  txmetcnp  22352  nmolb2d  22522  xrge0tsms  22637  metdsre  22656  metnrmlem3  22664  fsumcn  22673  elcncf2  22693  mulc1cncf  22708  cncfco  22710  cncfmet  22711  bndth  22757  evth  22758  copco  22818  pcopt2  22823  pcoass  22824  pcorevlem  22826  lmmcvg  23059  lmmbrf  23060  iscau4  23077  iscauf  23078  cmetcaulem  23086  iscmet3lem3  23088  iscmet3lem1  23089  causs  23096  equivcfil  23097  lmclim  23101  caubl  23106  caublcls  23107  bcth3  23128  ivthle  23225  ivthle2  23226  ovoliunlem1  23270  ovolicc2lem5  23289  volsuplem  23323  uniioombllem6  23356  dyaddisjlem  23363  dyadmax  23366  volcn  23374  mbfmulc2lem  23414  ismbf3d  23421  mbfsup  23431  mbfinf  23432  mbflim  23435  i1fmullem  23461  itg2seq  23509  itg2uba  23510  itg2splitlem  23515  itg2split  23516  itg2monolem1  23517  ditgsplitlem  23624  ellimc2  23641  ellimc3  23643  limcflf  23645  limcmpt  23647  limcco  23657  lhop1lem  23776  dvfsumle  23784  dvfsumabs  23786  dvfsumrlim  23794  ftc1a  23800  ftc1lem6  23804  mdegmullem  23838  elply2  23952  plypf1  23968  ulmcaulem  24148  ulmcau  24149  ulmss  24151  ulmdvlem3  24156  mtest  24158  itgulm  24162  abelthlem8  24193  abelth  24195  tanord  24284  cxpcn3lem  24488  mcubic  24574  cubic2  24575  dvdsflsumcom  24914  fsumdvdsmul  24921  lgsdchrval  25079  2sqlem9  25152  rplogsumlem2  25174  rpvmasumlem  25176  dchrvmasumlem1  25184  vmalogdivsum2  25227  logsqvma  25231  selberg  25237  selberg4  25250  pntibndlem3  25281  pntlem3  25298  pntleml  25300  padicabv  25319  padicabvf  25320  padicabvcxp  25321  ostth3  25327  axpasch  25821  axcontlem7  25850  axcontlem10  25853  cusgrsize2inds  26349  grpolcan  27384  nvmul0or  27505  nmosetre  27619  blocnilem  27659  blocni  27660  h2hcau  27836  h2hlm  27837  shsel3  28174  chscllem2  28497  homulcl  28618  adjsym  28692  cnvadj  28751  hhcno  28763  hhcnf  28764  lnopl  28773  unoplin  28779  counop  28780  lnfnl  28790  hmoplin  28801  hmopm  28880  nmcexi  28885  lnconi  28892  riesz3i  28921  leopmuli  28992  leopmul  28993  hstle  29089  mdsl0  29169  mdslmd1lem2  29185  atcvatlem  29244  chirredi  29253  cdj1i  29292  foresf1o  29343  isoun  29479  difioo  29544  xrge0tsmsd  29785  pstmxmet  29940  ordtrest2NEWlem  29968  esum2dlem  30154  esum2d  30155  dya2icoseg2  30340  eulerpartlemgc  30424  eulerpartlemgh  30440  eulerpartlemgs2  30442  ballotlemimin  30567  signstfvneq0  30649  hgt750lemb  30734  connpconn  31217  cvmliftmolem2  31264  cvmliftlem6  31272  cvmliftlem8  31274  cvmlift2lem12  31296  elmrsubrn  31417  elintfv  31662  dfon2lem6  31693  poseq  31750  nosupbnd1lem5  31858  nocvxminlem  31893  ifscgr  32151  brsegle  32215  neibastop2lem  32355  curf  33387  finixpnum  33394  fin2solem  33395  fin2so  33396  lindsenlbs  33404  matunitlindflem1  33405  matunitlindflem2  33406  matunitlindf  33407  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem14  33423  poimirlem16  33425  poimirlem19  33428  poimirlem22  33431  poimirlem28  33437  poimirlem29  33438  poimirlem30  33439  poimir  33442  heicant  33444  itg2gt0cn  33465  bddiblnc  33480  ftc1cnnc  33484  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anc  33493  cover2  33508  filbcmb  33535  fdc  33541  fdc1  33542  seqpo  33543  incsequz  33544  incsequz2  33545  metf1o  33551  lmclim2  33554  geomcau  33555  isbnd2  33582  bndss  33585  ismtybndlem  33605  heibor1lem  33608  rrncmslem  33631  rrnequiv  33634  exidreslem  33676  ghomco  33690  isdrngo3  33758  rngoisocnv  33780  isidlc  33814  idlnegcl  33821  divrngidl  33827  intidl  33828  unichnidl  33830  keridl  33831  igenmin  33863  prnc  33866  ispridlc  33869  prter3  34167  glbconxN  34664  atltcvr  34721  3dim1  34753  lvolnle3at  34868  linepsubN  35038  osumclN  35253  pexmidALTN  35264  lhpmatb  35317  cdlemg1idlemN  35860  dihlss  36539  dihglblem5aN  36581  dihatlat  36623  lsmfgcl  37644  kercvrlsm  37653  unxpwdom3  37665  hbt  37700  cntzsdrg  37772  cvgdvgrat  38512  climinf  39838  clim2f  39868  clim2cf  39882  clim0cf  39886  clim2f2  39902  fmtnofac2lem  41480  mgmhmpropd  41785  mgmhmima  41802  ovmpt2rdxf  42117  cotsqcscsq  42503  aacllem  42547