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  2551  2rexbidva  2553  ralimdvva  2599  pofun  4403  issod  4410  imainss  5144  fvelimab  5692  eqfnfv2  5735  funconstss  5755  fnex  5865  rexima  5884  ralima  5885  f1elima  5903  fliftfun  5926  isores2  5943  isosolem  5954  f1oiso  5956  ovmpodxf  6136  tfrlemibxssdm  6479  oav2  6617  omv2  6619  nnaass  6639  eroveu  6781  prarloclem4  7696  genpml  7715  genpmu  7716  genpassl  7722  genpassu  7723  prmuloc2  7765  addcomprg  7776  mulcomprg  7778  ltaddpr  7795  ltexprlemloc  7805  addcanprlemu  7813  recexgt0sr  7971  reapmul1  8753  apreim  8761  recexaplem2  8810  creur  9117  uz11  9757  xaddass  10077  xleadd1a  10081  xlt2add  10088  fzrevral  10313  seq3caopr2  10727  seqcaopr2g  10728  expnlbnd2  10899  shftlem  11342  resqrexlemgt0  11546  cau3lem  11640  clim2  11809  clim2c  11810  clim0c  11812  2clim  11827  climabs0  11833  climcn1  11834  climcn2  11835  climsqz  11861  climsqz2  11862  summodclem2  11908  fsum2dlemstep  11960  fsumiun  12003  mertenslem2  12062  mertensabs  12063  prodfrecap  12072  fprodeq0  12143  fprod2dlemstep  12148  gcdmultiplez  12557  dvdssq  12567  lcmgcdlem  12614  lcmdvds  12616  coprmdvds2  12630  pclemub  12825  pcxqcl  12850  pcge0  12851  pcgcd1  12866  prmpwdvds  12893  1arithlem4  12904  4sqlem18  12946  imasaddfnlemg  13362  imasaddflemg  13364  grpidpropdg  13422  grprida  13435  gsumpropd2  13441  mhmpropd  13514  mhmima  13539  grplcan  13610  dfgrp3mlem  13646  mulgdirlem  13705  subgmulg  13740  issubg4m  13745  subgintm  13750  ssnmz  13763  rngpropd  13933  srglmhm  13971  srgrmhm  13972  ringpropd  14016  ringlghm  14039  dvdsrpropdg  14126  isnzr2  14163  islmod  14270  islmodd  14272  lmodprop2d  14327  lsssubg  14356  lsspropdg  14410  lidlsubg  14465  expghmap  14586  neipsm  14843  lmbrf  14904  lmss  14935  txbas  14947  txbasval  14956  tx1cn  14958  txlm  14968  isxmet2d  15037  elmopn2  15138  mopni3  15173  blsscls2  15182  metequiv2  15185  metss2lem  15186  metrest  15195  metcnp  15201  metcnp2  15202  metcnpi3  15206  elcncf2  15263  mulc1cncf  15278  cncfco  15280  cncfmet  15281  fsumdvdsmul  15680  2sqlem9  15818