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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  anass  405  mpanr1  441  anass1rs  577  anabss5  584  anabss7  589  2ralbida  2571  2rexbidva  2573  ralimdvva  2619  pofun  4457  issod  4464  imainss  5203  fvelimab  5759  eqfnfv2  5807  funconstss  5827  fnex  5937  rexima  5960  ralima  5961  f1elima  5979  fliftfun  6002  isores2  6019  isosolem  6030  f1oiso  6032  ovmpodxf  6214  tfrlemibxssdm  6598  oav2  6736  omv2  6738  nnaass  6758  eroveu  6900  prarloclem4  7865  genpml  7884  genpmu  7885  genpassl  7891  genpassu  7892  prmuloc2  7934  addcomprg  7945  mulcomprg  7947  ltaddpr  7964  ltexprlemloc  7974  addcanprlemu  7982  recexgt0sr  8140  reapmul1  8925  apreim  8933  recexaplem2  8982  creur  9291  uz11  9954  xaddass  10281  xleadd1a  10285  xlt2add  10292  fzrevral  10522  seq3caopr2  10943  seqcaopr2g  10944  expnlbnd2  11116  shftlem  11595  resqrexlemgt0  11800  cau3lem  11895  clim2  12065  clim2c  12066  clim0c  12068  2clim  12083  climabs0  12089  climcn1  12090  climcn2  12091  climsqz  12117  climsqz2  12118  summodclem2  12165  fsum2dlemstep  12217  fsumiun  12260  mertenslem2  12319  mertensabs  12320  prodfrecap  12329  fprodeq0  12400  fprod2dlemstep  12405  gcdmultiplez  12814  dvdssq  12824  lcmgcdlem  12871  lcmdvds  12873  coprmdvds2  12887  pclemub  13086  pcxqcl  13111  pcge0  13112  pcgcd1  13127  prmpwdvds  13154  1arithlem4  13165  4sqlem18  13207  imasaddfnlemg  13684  imasaddflemg  13686  grpidpropdg  13743  grprida  13756  mhmpropd  13822  mhmima  13847  grplcan  13916  dfgrp3mlem  13952  mulgdirlem  14005  subgmulg  14040  issubg4m  14045  subgintm  14050  ssnmz  14063  rngpropd  14303  srglmhm  14346  srgrmhm  14347  ringpropd  14392  ringlghm  14415  dvdsrpropdg  14503  isnzr2  14540  islmod  14676  islmodd  14678  lmodprop2d  14734  lsssubg  14763  lsspropdg  14817  lidlsubg  14872  expghmap  14991  assapropd  15063  asclpropd  15089  neipsm  15304  lmbrf  15365  lmss  15396  txbas  15408  txbasval  15417  tx1cn  15419  txlm  15429  isxmet2d  15498  elmopn2  15599  mopni3  15634  blsscls2  15643  metequiv2  15646  metss2lem  15647  metrest  15656  metcnp  15662  metcnp2  15663  metcnpi3  15667  elcncf2  15724  mulc1cncf  15739  cncfco  15741  cncfmet  15742  zprmlogbaplem2  16135  fsumdvdsmul  16186  2sqlem9  16341