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  2498  2rexbidva  2500  ralimdvva  2546  pofun  4314  issod  4321  imainss  5046  fvelimab  5574  eqfnfv2  5616  funconstss  5636  fnex  5740  rexima  5757  ralima  5758  f1elima  5776  fliftfun  5799  isores2  5816  isosolem  5827  f1oiso  5829  ovmpodxf  6002  tfrlemibxssdm  6330  oav2  6466  omv2  6468  nnaass  6488  eroveu  6628  prarloclem4  7499  genpml  7518  genpmu  7519  genpassl  7525  genpassu  7526  prmuloc2  7568  addcomprg  7579  mulcomprg  7581  ltaddpr  7598  ltexprlemloc  7608  addcanprlemu  7616  recexgt0sr  7774  reapmul1  8554  apreim  8562  recexaplem2  8611  creur  8918  uz11  9552  xaddass  9871  xleadd1a  9875  xlt2add  9882  fzrevral  10107  seq3caopr2  10484  expnlbnd2  10648  shftlem  10827  resqrexlemgt0  11031  cau3lem  11125  clim2  11293  clim2c  11294  clim0c  11296  2clim  11311  climabs0  11317  climcn1  11318  climcn2  11319  climsqz  11345  climsqz2  11346  summodclem2  11392  fsum2dlemstep  11444  fsumiun  11487  mertenslem2  11546  mertensabs  11547  prodfrecap  11556  fprodeq0  11627  fprod2dlemstep  11632  gcdmultiplez  12024  dvdssq  12034  lcmgcdlem  12079  lcmdvds  12081  coprmdvds2  12095  pclemub  12289  pcge0  12314  pcgcd1  12329  prmpwdvds  12355  1arithlem4  12366  imasaddfnlemg  12740  imasaddflemg  12742  grpidpropdg  12798  grpridd  12811  mhmpropd  12862  mhmima  12880  grplcan  12937  dfgrp3mlem  12973  mulgdirlem  13019  subgmulg  13053  issubg4m  13058  subgintm  13063  ssnmz  13076  srglmhm  13181  srgrmhm  13182  ringpropd  13222  dvdsrpropdg  13321  islmod  13386  islmodd  13388  lmodprop2d  13443  lsssubg  13469  neipsm  13693  lmbrf  13754  lmss  13785  txbas  13797  txbasval  13806  tx1cn  13808  txlm  13818  isxmet2d  13887  elmopn2  13988  mopni3  14023  blsscls2  14032  metequiv2  14035  metss2lem  14036  metrest  14045  metcnp  14051  metcnp2  14052  metcnpi3  14056  elcncf2  14100  mulc1cncf  14115  cncfco  14117  cncfmet  14118  2sqlem9  14510