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  2526  2rexbidva  2528  ralimdvva  2574  pofun  4358  issod  4365  imainss  5097  fvelimab  5634  eqfnfv2  5677  funconstss  5697  fnex  5805  rexima  5822  ralima  5823  f1elima  5841  fliftfun  5864  isores2  5881  isosolem  5892  f1oiso  5894  ovmpodxf  6070  tfrlemibxssdm  6412  oav2  6548  omv2  6550  nnaass  6570  eroveu  6712  prarloclem4  7610  genpml  7629  genpmu  7630  genpassl  7636  genpassu  7637  prmuloc2  7679  addcomprg  7690  mulcomprg  7692  ltaddpr  7709  ltexprlemloc  7719  addcanprlemu  7727  recexgt0sr  7885  reapmul1  8667  apreim  8675  recexaplem2  8724  creur  9031  uz11  9670  xaddass  9990  xleadd1a  9994  xlt2add  10001  fzrevral  10226  seq3caopr2  10636  seqcaopr2g  10637  expnlbnd2  10808  shftlem  11098  resqrexlemgt0  11302  cau3lem  11396  clim2  11565  clim2c  11566  clim0c  11568  2clim  11583  climabs0  11589  climcn1  11590  climcn2  11591  climsqz  11617  climsqz2  11618  summodclem2  11664  fsum2dlemstep  11716  fsumiun  11759  mertenslem2  11818  mertensabs  11819  prodfrecap  11828  fprodeq0  11899  fprod2dlemstep  11904  gcdmultiplez  12313  dvdssq  12323  lcmgcdlem  12370  lcmdvds  12372  coprmdvds2  12386  pclemub  12581  pcxqcl  12606  pcge0  12607  pcgcd1  12622  prmpwdvds  12649  1arithlem4  12660  4sqlem18  12702  imasaddfnlemg  13117  imasaddflemg  13119  grpidpropdg  13177  grprida  13190  gsumpropd2  13196  mhmpropd  13269  mhmima  13294  grplcan  13365  dfgrp3mlem  13401  mulgdirlem  13460  subgmulg  13495  issubg4m  13500  subgintm  13505  ssnmz  13518  rngpropd  13688  srglmhm  13726  srgrmhm  13727  ringpropd  13771  ringlghm  13794  dvdsrpropdg  13880  isnzr2  13917  islmod  14024  islmodd  14026  lmodprop2d  14081  lsssubg  14110  lsspropdg  14164  lidlsubg  14219  expghmap  14340  neipsm  14597  lmbrf  14658  lmss  14689  txbas  14701  txbasval  14710  tx1cn  14712  txlm  14722  isxmet2d  14791  elmopn2  14892  mopni3  14927  blsscls2  14936  metequiv2  14939  metss2lem  14940  metrest  14949  metcnp  14955  metcnp2  14956  metcnpi3  14960  elcncf2  15017  mulc1cncf  15032  cncfco  15034  cncfmet  15035  fsumdvdsmul  15434  2sqlem9  15572