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  2553  2rexbidva  2555  ralimdvva  2601  pofun  4409  issod  4416  imainss  5152  fvelimab  5702  eqfnfv2  5745  funconstss  5765  fnex  5875  rexima  5894  ralima  5895  f1elima  5913  fliftfun  5936  isores2  5953  isosolem  5964  f1oiso  5966  ovmpodxf  6146  tfrlemibxssdm  6492  oav2  6630  omv2  6632  nnaass  6652  eroveu  6794  prarloclem4  7717  genpml  7736  genpmu  7737  genpassl  7743  genpassu  7744  prmuloc2  7786  addcomprg  7797  mulcomprg  7799  ltaddpr  7816  ltexprlemloc  7826  addcanprlemu  7834  recexgt0sr  7992  reapmul1  8774  apreim  8782  recexaplem2  8831  creur  9138  uz11  9778  xaddass  10103  xleadd1a  10107  xlt2add  10114  fzrevral  10339  seq3caopr2  10754  seqcaopr2g  10755  expnlbnd2  10926  shftlem  11376  resqrexlemgt0  11580  cau3lem  11674  clim2  11843  clim2c  11844  clim0c  11846  2clim  11861  climabs0  11867  climcn1  11868  climcn2  11869  climsqz  11895  climsqz2  11896  summodclem2  11942  fsum2dlemstep  11994  fsumiun  12037  mertenslem2  12096  mertensabs  12097  prodfrecap  12106  fprodeq0  12177  fprod2dlemstep  12182  gcdmultiplez  12591  dvdssq  12601  lcmgcdlem  12648  lcmdvds  12650  coprmdvds2  12664  pclemub  12859  pcxqcl  12884  pcge0  12885  pcgcd1  12900  prmpwdvds  12927  1arithlem4  12938  4sqlem18  12980  imasaddfnlemg  13396  imasaddflemg  13398  grpidpropdg  13456  grprida  13469  gsumpropd2  13475  mhmpropd  13548  mhmima  13573  grplcan  13644  dfgrp3mlem  13680  mulgdirlem  13739  subgmulg  13774  issubg4m  13779  subgintm  13784  ssnmz  13797  rngpropd  13967  srglmhm  14005  srgrmhm  14006  ringpropd  14050  ringlghm  14073  dvdsrpropdg  14160  isnzr2  14197  islmod  14304  islmodd  14306  lmodprop2d  14361  lsssubg  14390  lsspropdg  14444  lidlsubg  14499  expghmap  14620  neipsm  14877  lmbrf  14938  lmss  14969  txbas  14981  txbasval  14990  tx1cn  14992  txlm  15002  isxmet2d  15071  elmopn2  15172  mopni3  15207  blsscls2  15216  metequiv2  15219  metss2lem  15220  metrest  15229  metcnp  15235  metcnp2  15236  metcnpi3  15240  elcncf2  15297  mulc1cncf  15312  cncfco  15314  cncfmet  15315  fsumdvdsmul  15714  2sqlem9  15852