Theorem anassrs 400

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 )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  anass  401  mpanr1  437  anass1rs  573  anabss5  580  anabss7  585  2ralbida  2553  2rexbidva  2555  ralimdvva  2601  pofun  4409  issod  4416  imainss  5152  fvelimab  5702  eqfnfv2  5745  funconstss  5765  fnex  5876  rexima  5895  ralima  5896  f1elima  5914  fliftfun  5937  isores2  5954  isosolem  5965  f1oiso  5967  ovmpodxf  6147  tfrlemibxssdm  6493  oav2  6631  omv2  6633  nnaass  6653  eroveu  6795  prarloclem4  7718  genpml  7737  genpmu  7738  genpassl  7744  genpassu  7745  prmuloc2  7787  addcomprg  7798  mulcomprg  7800  ltaddpr  7817  ltexprlemloc  7827  addcanprlemu  7835  recexgt0sr  7993  reapmul1  8775  apreim  8783  recexaplem2  8832  creur  9139  uz11  9779  xaddass  10104  xleadd1a  10108  xlt2add  10115  fzrevral  10340  seq3caopr2  10756  seqcaopr2g  10757  expnlbnd2  10928  shftlem  11394  resqrexlemgt0  11598  cau3lem  11692  clim2  11861  clim2c  11862  clim0c  11864  2clim  11879  climabs0  11885  climcn1  11886  climcn2  11887  climsqz  11913  climsqz2  11914  summodclem2  11961  fsum2dlemstep  12013  fsumiun  12056  mertenslem2  12115  mertensabs  12116  prodfrecap  12125  fprodeq0  12196  fprod2dlemstep  12201  gcdmultiplez  12610  dvdssq  12620  lcmgcdlem  12667  lcmdvds  12669  coprmdvds2  12683  pclemub  12878  pcxqcl  12903  pcge0  12904  pcgcd1  12919  prmpwdvds  12946  1arithlem4  12957  4sqlem18  12999  imasaddfnlemg  13415  imasaddflemg  13417  grpidpropdg  13475  grprida  13488  gsumpropd2  13494  mhmpropd  13567  mhmima  13592  grplcan  13663  dfgrp3mlem  13699  mulgdirlem  13758  subgmulg  13793  issubg4m  13798  subgintm  13803  ssnmz  13816  rngpropd  13987  srglmhm  14025  srgrmhm  14026  ringpropd  14070  ringlghm  14093  dvdsrpropdg  14180  isnzr2  14217  islmod  14324  islmodd  14326  lmodprop2d  14381  lsssubg  14410  lsspropdg  14464  lidlsubg  14519  expghmap  14640  neipsm  14897  lmbrf  14958  lmss  14989  txbas  15001  txbasval  15010  tx1cn  15012  txlm  15022  isxmet2d  15091  elmopn2  15192  mopni3  15227  blsscls2  15236  metequiv2  15239  metss2lem  15240  metrest  15249  metcnp  15255  metcnp2  15256  metcnpi3  15260  elcncf2  15317  mulc1cncf  15332  cncfco  15334  cncfmet  15335  fsumdvdsmul  15734  2sqlem9  15872