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  6602  oav2  6740  omv2  6742  nnaass  6762  eroveu  6904  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  9961  xaddass  10288  xleadd1a  10292  xlt2add  10299  fzrevral  10529  seq3caopr2  10951  seqcaopr2g  10952  expnlbnd2  11124  shftlem  11603  resqrexlemgt0  11808  cau3lem  11903  clim2  12074  clim2c  12075  clim0c  12077  2clim  12092  climabs0  12098  climcn1  12099  climcn2  12100  climsqz  12126  climsqz2  12127  summodclem2  12174  fsum2dlemstep  12226  fsumiun  12269  mertenslem2  12328  mertensabs  12329  prodfrecap  12338  fprodeq0  12409  fprod2dlemstep  12414  gcdmultiplez  12823  dvdssq  12833  lcmgcdlem  12880  lcmdvds  12882  coprmdvds2  12896  pclemub  13095  pcxqcl  13120  pcge0  13121  pcgcd1  13136  prmpwdvds  13163  1arithlem4  13174  4sqlem18  13216  imasaddfnlemg  13694  imasaddflemg  13696  grpidpropdg  13753  grprida  13766  mhmpropd  13832  mhmima  13857  grplcan  13926  dfgrp3mlem  13962  mulgdirlem  14015  subgmulg  14050  issubg4m  14055  subgintm  14060  ssnmz  14073  cntzsubg  14171  gsum2d2fi  14274  rngpropd  14361  srglmhm  14404  srgrmhm  14405  ringpropd  14450  ringlghm  14473  dvdsrpropdg  14563  isnzr2  14600  islmod  14736  islmodd  14738  lmodprop2d  14794  lsssubg  14823  lsspropdg  14877  lidlsubg  14932  expghmap  15051  assapropd  15123  asclpropd  15149  psrass1filem  15177  neipsm  15380  lmbrf  15441  lmss  15472  txbas  15484  txbasval  15493  tx1cn  15495  txlm  15505  isxmet2d  15574  elmopn2  15675  mopni3  15710  blsscls2  15719  metequiv2  15722  metss2lem  15723  metrest  15732  metcnp  15738  metcnp2  15739  metcnpi3  15743  elcncf2  15800  mulc1cncf  15815  cncfco  15817  cncfmet  15818  zprmlogbaplem2  16216  fsumdvdsmul  16285  2sqlem9  16448