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  7866  genpml  7885  genpmu  7886  genpassl  7892  genpassu  7893  prmuloc2  7935  addcomprg  7946  mulcomprg  7948  ltaddpr  7965  ltexprlemloc  7975  addcanprlemu  7983  recexgt0sr  8141  reapmul1  8926  apreim  8934  recexaplem2  8983  creur  9292  uz11  9955  xaddass  10282  xleadd1a  10286  xlt2add  10293  fzrevral  10523  seq3caopr2  10945  seqcaopr2g  10946  expnlbnd2  11118  shftlem  11597  resqrexlemgt0  11802  cau3lem  11897  clim2  12068  clim2c  12069  clim0c  12071  2clim  12086  climabs0  12092  climcn1  12093  climcn2  12094  climsqz  12120  climsqz2  12121  summodclem2  12168  fsum2dlemstep  12220  fsumiun  12263  mertenslem2  12322  mertensabs  12323  prodfrecap  12332  fprodeq0  12403  fprod2dlemstep  12408  gcdmultiplez  12817  dvdssq  12827  lcmgcdlem  12874  lcmdvds  12876  coprmdvds2  12890  pclemub  13089  pcxqcl  13114  pcge0  13115  pcgcd1  13130  prmpwdvds  13157  1arithlem4  13168  4sqlem18  13210  imasaddfnlemg  13688  imasaddflemg  13690  grpidpropdg  13747  grprida  13760  mhmpropd  13826  mhmima  13851  grplcan  13920  dfgrp3mlem  13956  mulgdirlem  14009  subgmulg  14044  issubg4m  14049  subgintm  14054  ssnmz  14067  cntzsubg  14165  rngpropd  14338  srglmhm  14381  srgrmhm  14382  ringpropd  14427  ringlghm  14450  dvdsrpropdg  14538  isnzr2  14575  islmod  14711  islmodd  14713  lmodprop2d  14769  lsssubg  14798  lsspropdg  14852  lidlsubg  14907  expghmap  15026  assapropd  15098  asclpropd  15124  neipsm  15346  lmbrf  15407  lmss  15438  txbas  15450  txbasval  15459  tx1cn  15461  txlm  15471  isxmet2d  15540  elmopn2  15641  mopni3  15676  blsscls2  15685  metequiv2  15688  metss2lem  15689  metrest  15698  metcnp  15704  metcnp2  15705  metcnpi3  15709  elcncf2  15766  mulc1cncf  15781  cncfco  15783  cncfmet  15784  zprmlogbaplem2  16177  fsumdvdsmul  16246  2sqlem9  16409