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 )

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  405  mpanr1  441  anass1rs  577  anabss5  584  anabss7  589  2ralbida  2571  2rexbidva  2573  ralimdvva  2619  pofun  4452  issod  4459  imainss  5198  fvelimab  5753  eqfnfv2  5798  funconstss  5818  fnex  5928  rexima  5950  ralima  5951  f1elima  5969  fliftfun  5992  isores2  6009  isosolem  6020  f1oiso  6022  ovmpodxf  6204  tfrlemibxssdm  6588  oav2  6726  omv2  6728  nnaass  6748  eroveu  6890  prarloclem4  7855  genpml  7874  genpmu  7875  genpassl  7881  genpassu  7882  prmuloc2  7924  addcomprg  7935  mulcomprg  7937  ltaddpr  7954  ltexprlemloc  7964  addcanprlemu  7972  recexgt0sr  8130  reapmul1  8913  apreim  8921  recexaplem2  8970  creur  9279  uz11  9924  xaddass  10250  xleadd1a  10254  xlt2add  10261  fzrevral  10490  seq3caopr2  10908  seqcaopr2g  10909  expnlbnd2  11081  shftlem  11559  resqrexlemgt0  11764  cau3lem  11858  clim2  12027  clim2c  12028  clim0c  12030  2clim  12045  climabs0  12051  climcn1  12052  climcn2  12053  climsqz  12079  climsqz2  12080  summodclem2  12127  fsum2dlemstep  12179  fsumiun  12222  mertenslem2  12281  mertensabs  12282  prodfrecap  12291  fprodeq0  12362  fprod2dlemstep  12367  gcdmultiplez  12776  dvdssq  12786  lcmgcdlem  12833  lcmdvds  12835  coprmdvds2  12849  pclemub  13044  pcxqcl  13069  pcge0  13070  pcgcd1  13085  prmpwdvds  13112  1arithlem4  13123  4sqlem18  13165  imasaddfnlemg  13612  imasaddflemg  13614  grpidpropdg  13671  grprida  13684  mhmpropd  13750  mhmima  13775  grplcan  13844  dfgrp3mlem  13880  mulgdirlem  13933  subgmulg  13968  issubg4m  13973  subgintm  13978  ssnmz  13991  rngpropd  14229  srglmhm  14271  srgrmhm  14272  ringpropd  14316  ringlghm  14339  dvdsrpropdg  14427  isnzr2  14464  islmod  14600  islmodd  14602  lmodprop2d  14657  lsssubg  14686  lsspropdg  14740  lidlsubg  14795  expghmap  14914  neipsm  15178  lmbrf  15239  lmss  15270  txbas  15282  txbasval  15291  tx1cn  15293  txlm  15303  isxmet2d  15372  elmopn2  15473  mopni3  15508  blsscls2  15517  metequiv2  15520  metss2lem  15521  metrest  15530  metcnp  15536  metcnp2  15537  metcnpi3  15541  elcncf2  15598  mulc1cncf  15613  cncfco  15615  cncfmet  15616  fsumdvdsmul  16019  2sqlem9  16157