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  2496  2rexbidva  2498  ralimdvva  2544  pofun  4306  issod  4313  imainss  5036  fvelimab  5564  eqfnfv2  5606  funconstss  5626  fnex  5730  rexima  5746  ralima  5747  f1elima  5764  fliftfun  5787  isores2  5804  isosolem  5815  f1oiso  5817  ovmpodxf  5990  tfrlemibxssdm  6318  oav2  6454  omv2  6456  nnaass  6476  eroveu  6616  prarloclem4  7472  genpml  7491  genpmu  7492  genpassl  7498  genpassu  7499  prmuloc2  7541  addcomprg  7552  mulcomprg  7554  ltaddpr  7571  ltexprlemloc  7581  addcanprlemu  7589  recexgt0sr  7747  reapmul1  8526  apreim  8534  recexaplem2  8582  creur  8889  uz11  9523  xaddass  9840  xleadd1a  9844  xlt2add  9851  fzrevral  10075  seq3caopr2  10452  expnlbnd2  10615  shftlem  10793  resqrexlemgt0  10997  cau3lem  11091  clim2  11259  clim2c  11260  clim0c  11262  2clim  11277  climabs0  11283  climcn1  11284  climcn2  11285  climsqz  11311  climsqz2  11312  summodclem2  11358  fsum2dlemstep  11410  fsumiun  11453  mertenslem2  11512  mertensabs  11513  prodfrecap  11522  fprodeq0  11593  fprod2dlemstep  11598  gcdmultiplez  11989  dvdssq  11999  lcmgcdlem  12044  lcmdvds  12046  coprmdvds2  12060  pclemub  12254  pcge0  12279  pcgcd1  12294  prmpwdvds  12320  1arithlem4  12331  grpidpropdg  12668  grpridd  12681  mhmpropd  12729  mhmima  12746  grplcan  12802  dfgrp3mlem  12838  mulgdirlem  12883  srglmhm  12982  srgrmhm  12983  ringpropd  13022  neipsm  13234  lmbrf  13295  lmss  13326  txbas  13338  txbasval  13347  tx1cn  13349  txlm  13359  isxmet2d  13428  elmopn2  13529  mopni3  13564  blsscls2  13573  metequiv2  13576  metss2lem  13577  metrest  13586  metcnp  13592  metcnp2  13593  metcnpi3  13597  elcncf2  13641  mulc1cncf  13656  cncfco  13658  cncfmet  13659  2sqlem9  14040