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  4438  issod  4445  imainss  5183  fvelimab  5738  eqfnfv2  5781  funconstss  5801  fnex  5911  rexima  5933  ralima  5934  f1elima  5952  fliftfun  5975  isores2  5992  isosolem  6003  f1oiso  6005  ovmpodxf  6187  tfrlemibxssdm  6571  oav2  6709  omv2  6711  nnaass  6731  eroveu  6873  prarloclem4  7829  genpml  7848  genpmu  7849  genpassl  7855  genpassu  7856  prmuloc2  7898  addcomprg  7909  mulcomprg  7911  ltaddpr  7928  ltexprlemloc  7938  addcanprlemu  7946  recexgt0sr  8104  reapmul1  8887  apreim  8895  recexaplem2  8944  creur  9253  uz11  9898  xaddass  10224  xleadd1a  10228  xlt2add  10235  fzrevral  10464  seq3caopr2  10882  seqcaopr2g  10883  expnlbnd2  11055  shftlem  11529  resqrexlemgt0  11733  cau3lem  11827  clim2  11996  clim2c  11997  clim0c  11999  2clim  12014  climabs0  12020  climcn1  12021  climcn2  12022  climsqz  12048  climsqz2  12049  summodclem2  12096  fsum2dlemstep  12148  fsumiun  12191  mertenslem2  12250  mertensabs  12251  prodfrecap  12260  fprodeq0  12331  fprod2dlemstep  12336  gcdmultiplez  12745  dvdssq  12755  lcmgcdlem  12802  lcmdvds  12804  coprmdvds2  12818  pclemub  13013  pcxqcl  13038  pcge0  13039  pcgcd1  13054  prmpwdvds  13081  1arithlem4  13092  4sqlem18  13134  imasaddfnlemg  13581  imasaddflemg  13583  grpidpropdg  13640  grprida  13653  gsumpropd2  13659  mhmpropd  13724  mhmima  13749  grplcan  13820  dfgrp3mlem  13856  mulgdirlem  13909  subgmulg  13944  issubg4m  13949  subgintm  13954  ssnmz  13967  rngpropd  14197  srglmhm  14239  srgrmhm  14240  ringpropd  14284  ringlghm  14307  dvdsrpropdg  14395  isnzr2  14432  islmod  14568  islmodd  14570  lmodprop2d  14625  lsssubg  14654  lsspropdg  14708  lidlsubg  14763  expghmap  14884  neipsm  15148  lmbrf  15209  lmss  15240  txbas  15252  txbasval  15261  tx1cn  15263  txlm  15273  isxmet2d  15342  elmopn2  15443  mopni3  15478  blsscls2  15487  metequiv2  15490  metss2lem  15491  metrest  15500  metcnp  15506  metcnp2  15507  metcnpi3  15511  elcncf2  15568  mulc1cncf  15583  cncfco  15585  cncfmet  15586  fsumdvdsmul  15988  2sqlem9  16126