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  573  anabss5  580  anabss7  585  2ralbida  2554  2rexbidva  2556  ralimdvva  2602  pofun  4415  issod  4422  imainss  5159  fvelimab  5711  eqfnfv2  5754  funconstss  5774  fnex  5884  rexima  5905  ralima  5906  f1elima  5924  fliftfun  5947  isores2  5964  isosolem  5975  f1oiso  5977  ovmpodxf  6157  tfrlemibxssdm  6536  oav2  6674  omv2  6676  nnaass  6696  eroveu  6838  prarloclem4  7761  genpml  7780  genpmu  7781  genpassl  7787  genpassu  7788  prmuloc2  7830  addcomprg  7841  mulcomprg  7843  ltaddpr  7860  ltexprlemloc  7870  addcanprlemu  7878  recexgt0sr  8036  reapmul1  8817  apreim  8825  recexaplem2  8874  creur  9181  uz11  9823  xaddass  10148  xleadd1a  10152  xlt2add  10159  fzrevral  10385  seq3caopr2  10801  seqcaopr2g  10802  expnlbnd2  10973  shftlem  11439  resqrexlemgt0  11643  cau3lem  11737  clim2  11906  clim2c  11907  clim0c  11909  2clim  11924  climabs0  11930  climcn1  11931  climcn2  11932  climsqz  11958  climsqz2  11959  summodclem2  12006  fsum2dlemstep  12058  fsumiun  12101  mertenslem2  12160  mertensabs  12161  prodfrecap  12170  fprodeq0  12241  fprod2dlemstep  12246  gcdmultiplez  12655  dvdssq  12665  lcmgcdlem  12712  lcmdvds  12714  coprmdvds2  12728  pclemub  12923  pcxqcl  12948  pcge0  12949  pcgcd1  12964  prmpwdvds  12991  1arithlem4  13002  4sqlem18  13044  imasaddfnlemg  13460  imasaddflemg  13462  grpidpropdg  13520  grprida  13533  gsumpropd2  13539  mhmpropd  13612  mhmima  13637  grplcan  13708  dfgrp3mlem  13744  mulgdirlem  13803  subgmulg  13838  issubg4m  13843  subgintm  13848  ssnmz  13861  rngpropd  14032  srglmhm  14070  srgrmhm  14071  ringpropd  14115  ringlghm  14138  dvdsrpropdg  14225  isnzr2  14262  islmod  14370  islmodd  14372  lmodprop2d  14427  lsssubg  14456  lsspropdg  14510  lidlsubg  14565  expghmap  14686  neipsm  14948  lmbrf  15009  lmss  15040  txbas  15052  txbasval  15061  tx1cn  15063  txlm  15073  isxmet2d  15142  elmopn2  15243  mopni3  15278  blsscls2  15287  metequiv2  15290  metss2lem  15291  metrest  15300  metcnp  15306  metcnp2  15307  metcnpi3  15311  elcncf2  15368  mulc1cncf  15383  cncfco  15385  cncfmet  15386  fsumdvdsmul  15788  2sqlem9  15926