Theorem anassrs 404

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 365	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp31 256	1 |- ( ( ( ph /\ ps ) /\ ch ) -> th )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  anass  405  mpanr1  441  anass1rs  577  anabss5  584  anabss7  589  2ralbida  2571  2rexbidva  2573  ralimdvva  2619  pofun  4459  issod  4466  imainss  5206  fvelimab  5762  eqfnfv2  5810  funconstss  5830  fnex  5940  rexima  5963  ralima  5964  f1elima  5982  fliftfun  6005  isores2  6022  isosolem  6033  f1oiso  6035  ovmpodxf  6217  tfrlemibxssdm  6603  oav2  6741  omv2  6743  nnaass  6763  eroveu  6905  prarloclem4  7871  genpml  7890  genpmu  7891  genpassl  7897  genpassu  7898  prmuloc2  7940  addcomprg  7951  mulcomprg  7953  ltaddpr  7970  ltexprlemloc  7980  addcanprlemu  7988  recexgt0sr  8146  reapmul1  8931  apreim  8939  recexaplem2  8988  creur  9297  uz11  9960  xaddass  10287  xleadd1a  10291  xlt2add  10298  fzrevral  10528  seq3caopr2  10950  seqcaopr2g  10951  expnlbnd2  11123  shftlem  11602  resqrexlemgt0  11807  cau3lem  11902  clim2  12073  clim2c  12074  clim0c  12076  2clim  12091  climabs0  12097  climcn1  12098  climcn2  12099  climsqz  12125  climsqz2  12126  summodclem2  12173  fsum2dlemstep  12225  fsumiun  12268  mertenslem2  12327  mertensabs  12328  prodfrecap  12337  fprodeq0  12408  fprod2dlemstep  12413  gcdmultiplez  12822  dvdssq  12832  lcmgcdlem  12879  lcmdvds  12881  coprmdvds2  12895  pclemub  13094  pcxqcl  13119  pcge0  13120  pcgcd1  13135  prmpwdvds  13162  1arithlem4  13173  4sqlem18  13215  imasaddfnlemg  13693  imasaddflemg  13695  grpidpropdg  13752  grprida  13765  mhmpropd  13831  mhmima  13856  grplcan  13925  dfgrp3mlem  13961  mulgdirlem  14014  subgmulg  14049  issubg4m  14054  subgintm  14059  ssnmz  14072  cntzsubg  14170  gsum2d2fi  14273  rngpropd  14360  srglmhm  14403  srgrmhm  14404  ringpropd  14449  ringlghm  14472  dvdsrpropdg  14562  isnzr2  14599  islmod  14735  islmodd  14737  lmodprop2d  14793  lsssubg  14822  lsspropdg  14876  lidlsubg  14931  expghmap  15050  assapropd  15122  asclpropd  15148  psrass1filem  15186  neipsm  15397  lmbrf  15458  lmss  15489  txbas  15501  txbasval  15510  tx1cn  15512  txlm  15522  isxmet2d  15591  elmopn2  15692  mopni3  15727  blsscls2  15736  metequiv2  15739  metss2lem  15740  metrest  15749  metcnp  15755  metcnp2  15756  metcnpi3  15760  elcncf2  15817  mulc1cncf  15832  cncfco  15834  cncfmet  15835  zprmlogbaplem2  16233  fsumdvdsmul  16302  2sqlem9  16465