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  571  anabss5  578  anabss7  583  2ralbida  2551  2rexbidva  2553  ralimdvva  2599  pofun  4407  issod  4414  imainss  5150  fvelimab  5698  eqfnfv2  5741  funconstss  5761  fnex  5871  rexima  5890  ralima  5891  f1elima  5909  fliftfun  5932  isores2  5949  isosolem  5960  f1oiso  5962  ovmpodxf  6142  tfrlemibxssdm  6488  oav2  6626  omv2  6628  nnaass  6648  eroveu  6790  prarloclem4  7711  genpml  7730  genpmu  7731  genpassl  7737  genpassu  7738  prmuloc2  7780  addcomprg  7791  mulcomprg  7793  ltaddpr  7810  ltexprlemloc  7820  addcanprlemu  7828  recexgt0sr  7986  reapmul1  8768  apreim  8776  recexaplem2  8825  creur  9132  uz11  9772  xaddass  10097  xleadd1a  10101  xlt2add  10108  fzrevral  10333  seq3caopr2  10748  seqcaopr2g  10749  expnlbnd2  10920  shftlem  11370  resqrexlemgt0  11574  cau3lem  11668  clim2  11837  clim2c  11838  clim0c  11840  2clim  11855  climabs0  11861  climcn1  11862  climcn2  11863  climsqz  11889  climsqz2  11890  summodclem2  11936  fsum2dlemstep  11988  fsumiun  12031  mertenslem2  12090  mertensabs  12091  prodfrecap  12100  fprodeq0  12171  fprod2dlemstep  12176  gcdmultiplez  12585  dvdssq  12595  lcmgcdlem  12642  lcmdvds  12644  coprmdvds2  12658  pclemub  12853  pcxqcl  12878  pcge0  12879  pcgcd1  12894  prmpwdvds  12921  1arithlem4  12932  4sqlem18  12974  imasaddfnlemg  13390  imasaddflemg  13392  grpidpropdg  13450  grprida  13463  gsumpropd2  13469  mhmpropd  13542  mhmima  13567  grplcan  13638  dfgrp3mlem  13674  mulgdirlem  13733  subgmulg  13768  issubg4m  13773  subgintm  13778  ssnmz  13791  rngpropd  13961  srglmhm  13999  srgrmhm  14000  ringpropd  14044  ringlghm  14067  dvdsrpropdg  14154  isnzr2  14191  islmod  14298  islmodd  14300  lmodprop2d  14355  lsssubg  14384  lsspropdg  14438  lidlsubg  14493  expghmap  14614  neipsm  14871  lmbrf  14932  lmss  14963  txbas  14975  txbasval  14984  tx1cn  14986  txlm  14996  isxmet2d  15065  elmopn2  15166  mopni3  15201  blsscls2  15210  metequiv2  15213  metss2lem  15214  metrest  15223  metcnp  15229  metcnp2  15230  metcnpi3  15234  elcncf2  15291  mulc1cncf  15306  cncfco  15308  cncfmet  15309  fsumdvdsmul  15708  2sqlem9  15846