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  4402  issod  4409  imainss  5143  fvelimab  5689  eqfnfv2  5732  funconstss  5752  fnex  5860  rexima  5877  ralima  5878  f1elima  5896  fliftfun  5919  isores2  5936  isosolem  5947  f1oiso  5949  ovmpodxf  6129  tfrlemibxssdm  6471  oav2  6607  omv2  6609  nnaass  6629  eroveu  6771  prarloclem4  7681  genpml  7700  genpmu  7701  genpassl  7707  genpassu  7708  prmuloc2  7750  addcomprg  7761  mulcomprg  7763  ltaddpr  7780  ltexprlemloc  7790  addcanprlemu  7798  recexgt0sr  7956  reapmul1  8738  apreim  8746  recexaplem2  8795  creur  9102  uz11  9741  xaddass  10061  xleadd1a  10065  xlt2add  10072  fzrevral  10297  seq3caopr2  10710  seqcaopr2g  10711  expnlbnd2  10882  shftlem  11322  resqrexlemgt0  11526  cau3lem  11620  clim2  11789  clim2c  11790  clim0c  11792  2clim  11807  climabs0  11813  climcn1  11814  climcn2  11815  climsqz  11841  climsqz2  11842  summodclem2  11888  fsum2dlemstep  11940  fsumiun  11983  mertenslem2  12042  mertensabs  12043  prodfrecap  12052  fprodeq0  12123  fprod2dlemstep  12128  gcdmultiplez  12537  dvdssq  12547  lcmgcdlem  12594  lcmdvds  12596  coprmdvds2  12610  pclemub  12805  pcxqcl  12830  pcge0  12831  pcgcd1  12846  prmpwdvds  12873  1arithlem4  12884  4sqlem18  12926  imasaddfnlemg  13342  imasaddflemg  13344  grpidpropdg  13402  grprida  13415  gsumpropd2  13421  mhmpropd  13494  mhmima  13519  grplcan  13590  dfgrp3mlem  13626  mulgdirlem  13685  subgmulg  13720  issubg4m  13725  subgintm  13730  ssnmz  13743  rngpropd  13913  srglmhm  13951  srgrmhm  13952  ringpropd  13996  ringlghm  14019  dvdsrpropdg  14105  isnzr2  14142  islmod  14249  islmodd  14251  lmodprop2d  14306  lsssubg  14335  lsspropdg  14389  lidlsubg  14444  expghmap  14565  neipsm  14822  lmbrf  14883  lmss  14914  txbas  14926  txbasval  14935  tx1cn  14937  txlm  14947  isxmet2d  15016  elmopn2  15117  mopni3  15152  blsscls2  15161  metequiv2  15164  metss2lem  15165  metrest  15174  metcnp  15180  metcnp2  15181  metcnpi3  15185  elcncf2  15242  mulc1cncf  15257  cncfco  15259  cncfmet  15260  fsumdvdsmul  15659  2sqlem9  15797