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  2563  2rexbidva  2565  ralimdvva  2611  pofun  4433  issod  4440  imainss  5178  fvelimab  5733  eqfnfv2  5776  funconstss  5796  fnex  5906  rexima  5927  ralima  5928  f1elima  5946  fliftfun  5969  isores2  5986  isosolem  5997  f1oiso  5999  ovmpodxf  6179  tfrlemibxssdm  6558  oav2  6696  omv2  6698  nnaass  6718  eroveu  6860  prarloclem4  7813  genpml  7832  genpmu  7833  genpassl  7839  genpassu  7840  prmuloc2  7882  addcomprg  7893  mulcomprg  7895  ltaddpr  7912  ltexprlemloc  7922  addcanprlemu  7930  recexgt0sr  8088  reapmul1  8869  apreim  8877  recexaplem2  8926  creur  9233  uz11  9877  xaddass  10202  xleadd1a  10206  xlt2add  10213  fzrevral  10439  seq3caopr2  10855  seqcaopr2g  10856  expnlbnd2  11027  shftlem  11501  resqrexlemgt0  11705  cau3lem  11799  clim2  11968  clim2c  11969  clim0c  11971  2clim  11986  climabs0  11992  climcn1  11993  climcn2  11994  climsqz  12020  climsqz2  12021  summodclem2  12068  fsum2dlemstep  12120  fsumiun  12163  mertenslem2  12222  mertensabs  12223  prodfrecap  12232  fprodeq0  12303  fprod2dlemstep  12308  gcdmultiplez  12717  dvdssq  12727  lcmgcdlem  12774  lcmdvds  12776  coprmdvds2  12790  pclemub  12985  pcxqcl  13010  pcge0  13011  pcgcd1  13026  prmpwdvds  13053  1arithlem4  13064  4sqlem18  13106  imasaddfnlemg  13527  imasaddflemg  13529  grpidpropdg  13587  grprida  13600  gsumpropd2  13606  mhmpropd  13679  mhmima  13704  grplcan  13775  dfgrp3mlem  13811  mulgdirlem  13870  subgmulg  13905  issubg4m  13910  subgintm  13915  ssnmz  13928  rngpropd  14099  srglmhm  14137  srgrmhm  14138  ringpropd  14182  ringlghm  14205  dvdsrpropdg  14292  isnzr2  14329  islmod  14439  islmodd  14441  lmodprop2d  14496  lsssubg  14525  lsspropdg  14579  lidlsubg  14634  expghmap  14755  neipsm  15019  lmbrf  15080  lmss  15111  txbas  15123  txbasval  15132  tx1cn  15134  txlm  15144  isxmet2d  15213  elmopn2  15314  mopni3  15349  blsscls2  15358  metequiv2  15361  metss2lem  15362  metrest  15371  metcnp  15377  metcnp2  15378  metcnpi3  15382  elcncf2  15439  mulc1cncf  15454  cncfco  15456  cncfmet  15457  fsumdvdsmul  15859  2sqlem9  15997