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  2518  2rexbidva  2520  ralimdvva  2566  pofun  4347  issod  4354  imainss  5085  fvelimab  5617  eqfnfv2  5660  funconstss  5680  fnex  5784  rexima  5801  ralima  5802  f1elima  5820  fliftfun  5843  isores2  5860  isosolem  5871  f1oiso  5873  ovmpodxf  6048  tfrlemibxssdm  6385  oav2  6521  omv2  6523  nnaass  6543  eroveu  6685  prarloclem4  7565  genpml  7584  genpmu  7585  genpassl  7591  genpassu  7592  prmuloc2  7634  addcomprg  7645  mulcomprg  7647  ltaddpr  7664  ltexprlemloc  7674  addcanprlemu  7682  recexgt0sr  7840  reapmul1  8622  apreim  8630  recexaplem2  8679  creur  8986  uz11  9624  xaddass  9944  xleadd1a  9948  xlt2add  9955  fzrevral  10180  seq3caopr2  10585  seqcaopr2g  10586  expnlbnd2  10757  shftlem  10981  resqrexlemgt0  11185  cau3lem  11279  clim2  11448  clim2c  11449  clim0c  11451  2clim  11466  climabs0  11472  climcn1  11473  climcn2  11474  climsqz  11500  climsqz2  11501  summodclem2  11547  fsum2dlemstep  11599  fsumiun  11642  mertenslem2  11701  mertensabs  11702  prodfrecap  11711  fprodeq0  11782  fprod2dlemstep  11787  gcdmultiplez  12188  dvdssq  12198  lcmgcdlem  12245  lcmdvds  12247  coprmdvds2  12261  pclemub  12456  pcxqcl  12481  pcge0  12482  pcgcd1  12497  prmpwdvds  12524  1arithlem4  12535  4sqlem18  12577  imasaddfnlemg  12957  imasaddflemg  12959  grpidpropdg  13017  grprida  13030  gsumpropd2  13036  mhmpropd  13098  mhmima  13123  grplcan  13194  dfgrp3mlem  13230  mulgdirlem  13283  subgmulg  13318  issubg4m  13323  subgintm  13328  ssnmz  13341  rngpropd  13511  srglmhm  13549  srgrmhm  13550  ringpropd  13594  ringlghm  13617  dvdsrpropdg  13703  isnzr2  13740  islmod  13847  islmodd  13849  lmodprop2d  13904  lsssubg  13933  lsspropdg  13987  lidlsubg  14042  expghmap  14163  neipsm  14390  lmbrf  14451  lmss  14482  txbas  14494  txbasval  14503  tx1cn  14505  txlm  14515  isxmet2d  14584  elmopn2  14685  mopni3  14720  blsscls2  14729  metequiv2  14732  metss2lem  14733  metrest  14742  metcnp  14748  metcnp2  14749  metcnpi3  14753  elcncf2  14810  mulc1cncf  14825  cncfco  14827  cncfmet  14828  fsumdvdsmul  15227  2sqlem9  15365