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  2515  2rexbidva  2517  ralimdvva  2563  pofun  4344  issod  4351  imainss  5082  fvelimab  5614  eqfnfv2  5657  funconstss  5677  fnex  5781  rexima  5798  ralima  5799  f1elima  5817  fliftfun  5840  isores2  5857  isosolem  5868  f1oiso  5870  ovmpodxf  6045  tfrlemibxssdm  6382  oav2  6518  omv2  6520  nnaass  6540  eroveu  6682  prarloclem4  7560  genpml  7579  genpmu  7580  genpassl  7586  genpassu  7587  prmuloc2  7629  addcomprg  7640  mulcomprg  7642  ltaddpr  7659  ltexprlemloc  7669  addcanprlemu  7677  recexgt0sr  7835  reapmul1  8616  apreim  8624  recexaplem2  8673  creur  8980  uz11  9618  xaddass  9938  xleadd1a  9942  xlt2add  9949  fzrevral  10174  seq3caopr2  10567  seqcaopr2g  10568  expnlbnd2  10739  shftlem  10963  resqrexlemgt0  11167  cau3lem  11261  clim2  11429  clim2c  11430  clim0c  11432  2clim  11447  climabs0  11453  climcn1  11454  climcn2  11455  climsqz  11481  climsqz2  11482  summodclem2  11528  fsum2dlemstep  11580  fsumiun  11623  mertenslem2  11682  mertensabs  11683  prodfrecap  11692  fprodeq0  11763  fprod2dlemstep  11768  gcdmultiplez  12161  dvdssq  12171  lcmgcdlem  12218  lcmdvds  12220  coprmdvds2  12234  pclemub  12428  pcxqcl  12453  pcge0  12454  pcgcd1  12469  prmpwdvds  12496  1arithlem4  12507  4sqlem18  12549  imasaddfnlemg  12900  imasaddflemg  12902  grpidpropdg  12960  grprida  12973  gsumpropd2  12979  mhmpropd  13041  mhmima  13066  grplcan  13137  dfgrp3mlem  13173  mulgdirlem  13226  subgmulg  13261  issubg4m  13266  subgintm  13271  ssnmz  13284  rngpropd  13454  srglmhm  13492  srgrmhm  13493  ringpropd  13537  ringlghm  13560  dvdsrpropdg  13646  isnzr2  13683  islmod  13790  islmodd  13792  lmodprop2d  13847  lsssubg  13876  lsspropdg  13930  lidlsubg  13985  expghmap  14106  neipsm  14333  lmbrf  14394  lmss  14425  txbas  14437  txbasval  14446  tx1cn  14448  txlm  14458  isxmet2d  14527  elmopn2  14628  mopni3  14663  blsscls2  14672  metequiv2  14675  metss2lem  14676  metrest  14685  metcnp  14691  metcnp2  14692  metcnpi3  14696  elcncf2  14753  mulc1cncf  14768  cncfco  14770  cncfmet  14771  2sqlem9  15281