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  2565  2rexbidva  2567  ralimdvva  2613  pofun  4438  issod  4445  imainss  5183  fvelimab  5738  eqfnfv2  5781  funconstss  5801  fnex  5911  rexima  5933  ralima  5934  f1elima  5952  fliftfun  5975  isores2  5992  isosolem  6003  f1oiso  6005  ovmpodxf  6187  tfrlemibxssdm  6571  oav2  6709  omv2  6711  nnaass  6731  eroveu  6873  prarloclem4  7829  genpml  7848  genpmu  7849  genpassl  7855  genpassu  7856  prmuloc2  7898  addcomprg  7909  mulcomprg  7911  ltaddpr  7928  ltexprlemloc  7938  addcanprlemu  7946  recexgt0sr  8104  reapmul1  8886  apreim  8894  recexaplem2  8943  creur  9250  uz11  9895  xaddass  10221  xleadd1a  10225  xlt2add  10232  fzrevral  10461  seq3caopr2  10879  seqcaopr2g  10880  expnlbnd2  11052  shftlem  11526  resqrexlemgt0  11730  cau3lem  11824  clim2  11993  clim2c  11994  clim0c  11996  2clim  12011  climabs0  12017  climcn1  12018  climcn2  12019  climsqz  12045  climsqz2  12046  summodclem2  12093  fsum2dlemstep  12145  fsumiun  12188  mertenslem2  12247  mertensabs  12248  prodfrecap  12257  fprodeq0  12328  fprod2dlemstep  12333  gcdmultiplez  12742  dvdssq  12752  lcmgcdlem  12799  lcmdvds  12801  coprmdvds2  12815  pclemub  13010  pcxqcl  13035  pcge0  13036  pcgcd1  13051  prmpwdvds  13078  1arithlem4  13089  4sqlem18  13131  imasaddfnlemg  13578  imasaddflemg  13580  grpidpropdg  13637  grprida  13650  gsumpropd2  13656  mhmpropd  13721  mhmima  13746  grplcan  13817  dfgrp3mlem  13853  mulgdirlem  13906  subgmulg  13941  issubg4m  13946  subgintm  13951  ssnmz  13964  rngpropd  14194  srglmhm  14236  srgrmhm  14237  ringpropd  14281  ringlghm  14304  dvdsrpropdg  14392  isnzr2  14429  islmod  14565  islmodd  14567  lmodprop2d  14622  lsssubg  14651  lsspropdg  14705  lidlsubg  14760  expghmap  14881  neipsm  15145  lmbrf  15206  lmss  15237  txbas  15249  txbasval  15258  tx1cn  15260  txlm  15270  isxmet2d  15339  elmopn2  15440  mopni3  15475  blsscls2  15484  metequiv2  15487  metss2lem  15488  metrest  15497  metcnp  15503  metcnp2  15504  metcnpi3  15508  elcncf2  15565  mulc1cncf  15580  cncfco  15582  cncfmet  15583  fsumdvdsmul  15985  2sqlem9  16123