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  4457  issod  4464  imainss  5203  fvelimab  5759  eqfnfv2  5807  funconstss  5827  fnex  5937  rexima  5960  ralima  5961  f1elima  5979  fliftfun  6002  isores2  6019  isosolem  6030  f1oiso  6032  ovmpodxf  6214  tfrlemibxssdm  6598  oav2  6736  omv2  6738  nnaass  6758  eroveu  6900  prarloclem4  7865  genpml  7884  genpmu  7885  genpassl  7891  genpassu  7892  prmuloc2  7934  addcomprg  7945  mulcomprg  7947  ltaddpr  7964  ltexprlemloc  7974  addcanprlemu  7982  recexgt0sr  8140  reapmul1  8923  apreim  8931  recexaplem2  8980  creur  9289  uz11  9945  xaddass  10271  xleadd1a  10275  xlt2add  10282  fzrevral  10512  seq3caopr2  10930  seqcaopr2g  10931  expnlbnd2  11103  shftlem  11581  resqrexlemgt0  11786  cau3lem  11880  clim2  12049  clim2c  12050  clim0c  12052  2clim  12067  climabs0  12073  climcn1  12074  climcn2  12075  climsqz  12101  climsqz2  12102  summodclem2  12149  fsum2dlemstep  12201  fsumiun  12244  mertenslem2  12303  mertensabs  12304  prodfrecap  12313  fprodeq0  12384  fprod2dlemstep  12389  gcdmultiplez  12798  dvdssq  12808  lcmgcdlem  12855  lcmdvds  12857  coprmdvds2  12871  pclemub  13066  pcxqcl  13091  pcge0  13092  pcgcd1  13107  prmpwdvds  13134  1arithlem4  13145  4sqlem18  13187  imasaddfnlemg  13635  imasaddflemg  13637  grpidpropdg  13694  grprida  13707  mhmpropd  13773  mhmima  13798  grplcan  13867  dfgrp3mlem  13903  mulgdirlem  13956  subgmulg  13991  issubg4m  13996  subgintm  14001  ssnmz  14014  rngpropd  14254  srglmhm  14297  srgrmhm  14298  ringpropd  14343  ringlghm  14366  dvdsrpropdg  14454  isnzr2  14491  islmod  14627  islmodd  14629  lmodprop2d  14685  lsssubg  14714  lsspropdg  14768  lidlsubg  14823  expghmap  14942  assapropd  15014  asclpropd  15040  neipsm  15255  lmbrf  15316  lmss  15347  txbas  15359  txbasval  15368  tx1cn  15370  txlm  15380  isxmet2d  15449  elmopn2  15550  mopni3  15585  blsscls2  15594  metequiv2  15597  metss2lem  15598  metrest  15607  metcnp  15613  metcnp2  15614  metcnpi3  15618  elcncf2  15675  mulc1cncf  15690  cncfco  15692  cncfmet  15693  fsumdvdsmul  16105  2sqlem9  16243