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  2563  2rexbidva  2565  ralimdvva  2611  pofun  4432  issod  4439  imainss  5177  fvelimab  5732  eqfnfv2  5775  funconstss  5795  fnex  5905  rexima  5926  ralima  5927  f1elima  5945  fliftfun  5968  isores2  5985  isosolem  5996  f1oiso  5998  ovmpodxf  6178  tfrlemibxssdm  6557  oav2  6695  omv2  6697  nnaass  6717  eroveu  6859  prarloclem4  7812  genpml  7831  genpmu  7832  genpassl  7838  genpassu  7839  prmuloc2  7881  addcomprg  7892  mulcomprg  7894  ltaddpr  7911  ltexprlemloc  7921  addcanprlemu  7929  recexgt0sr  8087  reapmul1  8868  apreim  8876  recexaplem2  8925  creur  9232  uz11  9876  xaddass  10201  xleadd1a  10205  xlt2add  10212  fzrevral  10438  seq3caopr2  10854  seqcaopr2g  10855  expnlbnd2  11026  shftlem  11497  resqrexlemgt0  11701  cau3lem  11795  clim2  11964  clim2c  11965  clim0c  11967  2clim  11982  climabs0  11988  climcn1  11989  climcn2  11990  climsqz  12016  climsqz2  12017  summodclem2  12064  fsum2dlemstep  12116  fsumiun  12159  mertenslem2  12218  mertensabs  12219  prodfrecap  12228  fprodeq0  12299  fprod2dlemstep  12304  gcdmultiplez  12713  dvdssq  12723  lcmgcdlem  12770  lcmdvds  12772  coprmdvds2  12786  pclemub  12981  pcxqcl  13006  pcge0  13007  pcgcd1  13022  prmpwdvds  13049  1arithlem4  13060  4sqlem18  13102  imasaddfnlemg  13519  imasaddflemg  13521  grpidpropdg  13579  grprida  13592  gsumpropd2  13598  mhmpropd  13671  mhmima  13696  grplcan  13767  dfgrp3mlem  13803  mulgdirlem  13862  subgmulg  13897  issubg4m  13902  subgintm  13907  ssnmz  13920  rngpropd  14091  srglmhm  14129  srgrmhm  14130  ringpropd  14174  ringlghm  14197  dvdsrpropdg  14284  isnzr2  14321  islmod  14431  islmodd  14433  lmodprop2d  14488  lsssubg  14517  lsspropdg  14571  lidlsubg  14626  expghmap  14747  neipsm  15011  lmbrf  15072  lmss  15103  txbas  15115  txbasval  15124  tx1cn  15126  txlm  15136  isxmet2d  15205  elmopn2  15306  mopni3  15341  blsscls2  15350  metequiv2  15353  metss2lem  15354  metrest  15363  metcnp  15369  metcnp2  15370  metcnpi3  15374  elcncf2  15431  mulc1cncf  15446  cncfco  15448  cncfmet  15449  fsumdvdsmul  15851  2sqlem9  15989