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  571  anabss5  578  anabss7  583  2ralbida  2527  2rexbidva  2529  ralimdvva  2575  pofun  4359  issod  4366  imainss  5098  fvelimab  5635  eqfnfv2  5678  funconstss  5698  fnex  5806  rexima  5823  ralima  5824  f1elima  5842  fliftfun  5865  isores2  5882  isosolem  5893  f1oiso  5895  ovmpodxf  6071  tfrlemibxssdm  6413  oav2  6549  omv2  6551  nnaass  6571  eroveu  6713  prarloclem4  7611  genpml  7630  genpmu  7631  genpassl  7637  genpassu  7638  prmuloc2  7680  addcomprg  7691  mulcomprg  7693  ltaddpr  7710  ltexprlemloc  7720  addcanprlemu  7728  recexgt0sr  7886  reapmul1  8668  apreim  8676  recexaplem2  8725  creur  9032  uz11  9671  xaddass  9991  xleadd1a  9995  xlt2add  10002  fzrevral  10227  seq3caopr2  10638  seqcaopr2g  10639  expnlbnd2  10810  shftlem  11127  resqrexlemgt0  11331  cau3lem  11425  clim2  11594  clim2c  11595  clim0c  11597  2clim  11612  climabs0  11618  climcn1  11619  climcn2  11620  climsqz  11646  climsqz2  11647  summodclem2  11693  fsum2dlemstep  11745  fsumiun  11788  mertenslem2  11847  mertensabs  11848  prodfrecap  11857  fprodeq0  11928  fprod2dlemstep  11933  gcdmultiplez  12342  dvdssq  12352  lcmgcdlem  12399  lcmdvds  12401  coprmdvds2  12415  pclemub  12610  pcxqcl  12635  pcge0  12636  pcgcd1  12651  prmpwdvds  12678  1arithlem4  12689  4sqlem18  12731  imasaddfnlemg  13146  imasaddflemg  13148  grpidpropdg  13206  grprida  13219  gsumpropd2  13225  mhmpropd  13298  mhmima  13323  grplcan  13394  dfgrp3mlem  13430  mulgdirlem  13489  subgmulg  13524  issubg4m  13529  subgintm  13534  ssnmz  13547  rngpropd  13717  srglmhm  13755  srgrmhm  13756  ringpropd  13800  ringlghm  13823  dvdsrpropdg  13909  isnzr2  13946  islmod  14053  islmodd  14055  lmodprop2d  14110  lsssubg  14139  lsspropdg  14193  lidlsubg  14248  expghmap  14369  neipsm  14626  lmbrf  14687  lmss  14718  txbas  14730  txbasval  14739  tx1cn  14741  txlm  14751  isxmet2d  14820  elmopn2  14921  mopni3  14956  blsscls2  14965  metequiv2  14968  metss2lem  14969  metrest  14978  metcnp  14984  metcnp2  14985  metcnpi3  14989  elcncf2  15046  mulc1cncf  15061  cncfco  15063  cncfmet  15064  fsumdvdsmul  15463  2sqlem9  15601