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  4343  issod  4350  imainss  5081  fvelimab  5613  eqfnfv2  5656  funconstss  5676  fnex  5780  rexima  5797  ralima  5798  f1elima  5816  fliftfun  5839  isores2  5856  isosolem  5867  f1oiso  5869  ovmpodxf  6044  tfrlemibxssdm  6380  oav2  6516  omv2  6518  nnaass  6538  eroveu  6680  prarloclem4  7558  genpml  7577  genpmu  7578  genpassl  7584  genpassu  7585  prmuloc2  7627  addcomprg  7638  mulcomprg  7640  ltaddpr  7657  ltexprlemloc  7667  addcanprlemu  7675  recexgt0sr  7833  reapmul1  8614  apreim  8622  recexaplem2  8671  creur  8978  uz11  9615  xaddass  9935  xleadd1a  9939  xlt2add  9946  fzrevral  10171  seq3caopr2  10564  seqcaopr2g  10565  expnlbnd2  10736  shftlem  10960  resqrexlemgt0  11164  cau3lem  11258  clim2  11426  clim2c  11427  clim0c  11429  2clim  11444  climabs0  11450  climcn1  11451  climcn2  11452  climsqz  11478  climsqz2  11479  summodclem2  11525  fsum2dlemstep  11577  fsumiun  11620  mertenslem2  11679  mertensabs  11680  prodfrecap  11689  fprodeq0  11760  fprod2dlemstep  11765  gcdmultiplez  12158  dvdssq  12168  lcmgcdlem  12215  lcmdvds  12217  coprmdvds2  12231  pclemub  12425  pcxqcl  12450  pcge0  12451  pcgcd1  12466  prmpwdvds  12493  1arithlem4  12504  4sqlem18  12546  imasaddfnlemg  12897  imasaddflemg  12899  grpidpropdg  12957  grprida  12970  gsumpropd2  12976  mhmpropd  13038  mhmima  13063  grplcan  13134  dfgrp3mlem  13170  mulgdirlem  13223  subgmulg  13258  issubg4m  13263  subgintm  13268  ssnmz  13281  rngpropd  13451  srglmhm  13489  srgrmhm  13490  ringpropd  13534  ringlghm  13557  dvdsrpropdg  13643  isnzr2  13680  islmod  13787  islmodd  13789  lmodprop2d  13844  lsssubg  13873  lsspropdg  13927  lidlsubg  13982  expghmap  14095  neipsm  14322  lmbrf  14383  lmss  14414  txbas  14426  txbasval  14435  tx1cn  14437  txlm  14447  isxmet2d  14516  elmopn2  14617  mopni3  14652  blsscls2  14661  metequiv2  14664  metss2lem  14665  metrest  14674  metcnp  14680  metcnp2  14681  metcnpi3  14685  elcncf2  14729  mulc1cncf  14744  cncfco  14746  cncfmet  14747  2sqlem9  15211