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  2551  2rexbidva  2553  ralimdvva  2599  pofun  4407  issod  4414  imainss  5150  fvelimab  5698  eqfnfv2  5741  funconstss  5761  fnex  5871  rexima  5890  ralima  5891  f1elima  5909  fliftfun  5932  isores2  5949  isosolem  5960  f1oiso  5962  ovmpodxf  6142  tfrlemibxssdm  6488  oav2  6626  omv2  6628  nnaass  6648  eroveu  6790  prarloclem4  7708  genpml  7727  genpmu  7728  genpassl  7734  genpassu  7735  prmuloc2  7777  addcomprg  7788  mulcomprg  7790  ltaddpr  7807  ltexprlemloc  7817  addcanprlemu  7825  recexgt0sr  7983  reapmul1  8765  apreim  8773  recexaplem2  8822  creur  9129  uz11  9769  xaddass  10094  xleadd1a  10098  xlt2add  10105  fzrevral  10330  seq3caopr2  10745  seqcaopr2g  10746  expnlbnd2  10917  shftlem  11367  resqrexlemgt0  11571  cau3lem  11665  clim2  11834  clim2c  11835  clim0c  11837  2clim  11852  climabs0  11858  climcn1  11859  climcn2  11860  climsqz  11886  climsqz2  11887  summodclem2  11933  fsum2dlemstep  11985  fsumiun  12028  mertenslem2  12087  mertensabs  12088  prodfrecap  12097  fprodeq0  12168  fprod2dlemstep  12173  gcdmultiplez  12582  dvdssq  12592  lcmgcdlem  12639  lcmdvds  12641  coprmdvds2  12655  pclemub  12850  pcxqcl  12875  pcge0  12876  pcgcd1  12891  prmpwdvds  12918  1arithlem4  12929  4sqlem18  12971  imasaddfnlemg  13387  imasaddflemg  13389  grpidpropdg  13447  grprida  13460  gsumpropd2  13466  mhmpropd  13539  mhmima  13564  grplcan  13635  dfgrp3mlem  13671  mulgdirlem  13730  subgmulg  13765  issubg4m  13770  subgintm  13775  ssnmz  13788  rngpropd  13958  srglmhm  13996  srgrmhm  13997  ringpropd  14041  ringlghm  14064  dvdsrpropdg  14151  isnzr2  14188  islmod  14295  islmodd  14297  lmodprop2d  14352  lsssubg  14381  lsspropdg  14435  lidlsubg  14490  expghmap  14611  neipsm  14868  lmbrf  14929  lmss  14960  txbas  14972  txbasval  14981  tx1cn  14983  txlm  14993  isxmet2d  15062  elmopn2  15163  mopni3  15198  blsscls2  15207  metequiv2  15210  metss2lem  15211  metrest  15220  metcnp  15226  metcnp2  15227  metcnpi3  15231  elcncf2  15288  mulc1cncf  15303  cncfco  15305  cncfmet  15306  fsumdvdsmul  15705  2sqlem9  15843