Theorem anassrs 400

Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
anassrs.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
anassrs	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem anassrs

Step	Hyp	Ref	Expression
1		anassrs.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 365	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 256	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

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  2565  2rexbidva  2567  ralimdvva  2613  pofun  4435  issod  4442  imainss  5180  fvelimab  5735  eqfnfv2  5778  funconstss  5798  fnex  5908  rexima  5929  ralima  5930  f1elima  5948  fliftfun  5971  isores2  5988  isosolem  5999  f1oiso  6001  ovmpodxf  6181  tfrlemibxssdm  6560  oav2  6698  omv2  6700  nnaass  6720  eroveu  6862  prarloclem4  7818  genpml  7837  genpmu  7838  genpassl  7844  genpassu  7845  prmuloc2  7887  addcomprg  7898  mulcomprg  7900  ltaddpr  7917  ltexprlemloc  7927  addcanprlemu  7935  recexgt0sr  8093  reapmul1  8874  apreim  8882  recexaplem2  8931  creur  9238  uz11  9883  xaddass  10208  xleadd1a  10212  xlt2add  10219  fzrevral  10446  seq3caopr2  10862  seqcaopr2g  10863  expnlbnd2  11035  shftlem  11509  resqrexlemgt0  11713  cau3lem  11807  clim2  11976  clim2c  11977  clim0c  11979  2clim  11994  climabs0  12000  climcn1  12001  climcn2  12002  climsqz  12028  climsqz2  12029  summodclem2  12076  fsum2dlemstep  12128  fsumiun  12171  mertenslem2  12230  mertensabs  12231  prodfrecap  12240  fprodeq0  12311  fprod2dlemstep  12316  gcdmultiplez  12725  dvdssq  12735  lcmgcdlem  12782  lcmdvds  12784  coprmdvds2  12798  pclemub  12993  pcxqcl  13018  pcge0  13019  pcgcd1  13034  prmpwdvds  13061  1arithlem4  13072  4sqlem18  13114  imasaddfnlemg  13548  imasaddflemg  13550  grpidpropdg  13608  grprida  13621  gsumpropd2  13627  mhmpropd  13700  mhmima  13725  grplcan  13796  dfgrp3mlem  13832  mulgdirlem  13891  subgmulg  13926  issubg4m  13931  subgintm  13936  ssnmz  13949  rngpropd  14120  srglmhm  14158  srgrmhm  14159  ringpropd  14203  ringlghm  14226  dvdsrpropdg  14314  isnzr2  14351  islmod  14488  islmodd  14490  lmodprop2d  14545  lsssubg  14574  lsspropdg  14628  lidlsubg  14683  expghmap  14804  neipsm  15068  lmbrf  15129  lmss  15160  txbas  15172  txbasval  15181  tx1cn  15183  txlm  15193  isxmet2d  15262  elmopn2  15363  mopni3  15398  blsscls2  15407  metequiv2  15410  metss2lem  15411  metrest  15420  metcnp  15426  metcnp2  15427  metcnpi3  15431  elcncf2  15488  mulc1cncf  15503  cncfco  15505  cncfmet  15506  fsumdvdsmul  15908  2sqlem9  16046