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  2508  2rexbidva  2510  ralimdvva  2556  pofun  4324  issod  4331  imainss  5056  fvelimab  5585  eqfnfv2  5627  funconstss  5647  fnex  5751  rexima  5768  ralima  5769  f1elima  5787  fliftfun  5810  isores2  5827  isosolem  5838  f1oiso  5840  ovmpodxf  6014  tfrlemibxssdm  6342  oav2  6478  omv2  6480  nnaass  6500  eroveu  6640  prarloclem4  7511  genpml  7530  genpmu  7531  genpassl  7537  genpassu  7538  prmuloc2  7580  addcomprg  7591  mulcomprg  7593  ltaddpr  7610  ltexprlemloc  7620  addcanprlemu  7628  recexgt0sr  7786  reapmul1  8566  apreim  8574  recexaplem2  8623  creur  8930  uz11  9564  xaddass  9883  xleadd1a  9887  xlt2add  9894  fzrevral  10119  seq3caopr2  10496  expnlbnd2  10660  shftlem  10839  resqrexlemgt0  11043  cau3lem  11137  clim2  11305  clim2c  11306  clim0c  11308  2clim  11323  climabs0  11329  climcn1  11330  climcn2  11331  climsqz  11357  climsqz2  11358  summodclem2  11404  fsum2dlemstep  11456  fsumiun  11499  mertenslem2  11558  mertensabs  11559  prodfrecap  11568  fprodeq0  11639  fprod2dlemstep  11644  gcdmultiplez  12036  dvdssq  12046  lcmgcdlem  12091  lcmdvds  12093  coprmdvds2  12107  pclemub  12301  pcge0  12326  pcgcd1  12341  prmpwdvds  12367  1arithlem4  12378  imasaddfnlemg  12753  imasaddflemg  12755  grpidpropdg  12812  grprida  12825  mhmpropd  12879  mhmima  12904  grplcan  12967  dfgrp3mlem  13003  mulgdirlem  13054  subgmulg  13088  issubg4m  13093  subgintm  13098  ssnmz  13111  rngpropd  13264  srglmhm  13302  srgrmhm  13303  ringpropd  13347  dvdsrpropdg  13452  islmod  13537  islmodd  13539  lmodprop2d  13594  lsssubg  13623  lsspropdg  13677  lidlsubg  13732  neipsm  14007  lmbrf  14068  lmss  14099  txbas  14111  txbasval  14120  tx1cn  14122  txlm  14132  isxmet2d  14201  elmopn2  14302  mopni3  14337  blsscls2  14346  metequiv2  14349  metss2lem  14350  metrest  14359  metcnp  14365  metcnp2  14366  metcnpi3  14370  elcncf2  14414  mulc1cncf  14429  cncfco  14431  cncfmet  14432  2sqlem9  14824