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  2529  2rexbidva  2531  ralimdvva  2577  pofun  4377  issod  4384  imainss  5117  fvelimab  5658  eqfnfv2  5701  funconstss  5721  fnex  5829  rexima  5846  ralima  5847  f1elima  5865  fliftfun  5888  isores2  5905  isosolem  5916  f1oiso  5918  ovmpodxf  6094  tfrlemibxssdm  6436  oav2  6572  omv2  6574  nnaass  6594  eroveu  6736  prarloclem4  7646  genpml  7665  genpmu  7666  genpassl  7672  genpassu  7673  prmuloc2  7715  addcomprg  7726  mulcomprg  7728  ltaddpr  7745  ltexprlemloc  7755  addcanprlemu  7763  recexgt0sr  7921  reapmul1  8703  apreim  8711  recexaplem2  8760  creur  9067  uz11  9706  xaddass  10026  xleadd1a  10030  xlt2add  10037  fzrevral  10262  seq3caopr2  10675  seqcaopr2g  10676  expnlbnd2  10847  shftlem  11242  resqrexlemgt0  11446  cau3lem  11540  clim2  11709  clim2c  11710  clim0c  11712  2clim  11727  climabs0  11733  climcn1  11734  climcn2  11735  climsqz  11761  climsqz2  11762  summodclem2  11808  fsum2dlemstep  11860  fsumiun  11903  mertenslem2  11962  mertensabs  11963  prodfrecap  11972  fprodeq0  12043  fprod2dlemstep  12048  gcdmultiplez  12457  dvdssq  12467  lcmgcdlem  12514  lcmdvds  12516  coprmdvds2  12530  pclemub  12725  pcxqcl  12750  pcge0  12751  pcgcd1  12766  prmpwdvds  12793  1arithlem4  12804  4sqlem18  12846  imasaddfnlemg  13261  imasaddflemg  13263  grpidpropdg  13321  grprida  13334  gsumpropd2  13340  mhmpropd  13413  mhmima  13438  grplcan  13509  dfgrp3mlem  13545  mulgdirlem  13604  subgmulg  13639  issubg4m  13644  subgintm  13649  ssnmz  13662  rngpropd  13832  srglmhm  13870  srgrmhm  13871  ringpropd  13915  ringlghm  13938  dvdsrpropdg  14024  isnzr2  14061  islmod  14168  islmodd  14170  lmodprop2d  14225  lsssubg  14254  lsspropdg  14308  lidlsubg  14363  expghmap  14484  neipsm  14741  lmbrf  14802  lmss  14833  txbas  14845  txbasval  14854  tx1cn  14856  txlm  14866  isxmet2d  14935  elmopn2  15036  mopni3  15071  blsscls2  15080  metequiv2  15083  metss2lem  15084  metrest  15093  metcnp  15099  metcnp2  15100  metcnpi3  15104  elcncf2  15161  mulc1cncf  15176  cncfco  15178  cncfmet  15179  fsumdvdsmul  15578  2sqlem9  15716