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  2498  2rexbidva  2500  ralimdvva  2546  pofun  4312  issod  4319  imainss  5044  fvelimab  5572  eqfnfv2  5614  funconstss  5634  fnex  5738  rexima  5755  ralima  5756  f1elima  5773  fliftfun  5796  isores2  5813  isosolem  5824  f1oiso  5826  ovmpodxf  5999  tfrlemibxssdm  6327  oav2  6463  omv2  6465  nnaass  6485  eroveu  6625  prarloclem4  7496  genpml  7515  genpmu  7516  genpassl  7522  genpassu  7523  prmuloc2  7565  addcomprg  7576  mulcomprg  7578  ltaddpr  7595  ltexprlemloc  7605  addcanprlemu  7613  recexgt0sr  7771  reapmul1  8551  apreim  8559  recexaplem2  8608  creur  8915  uz11  9549  xaddass  9868  xleadd1a  9872  xlt2add  9879  fzrevral  10104  seq3caopr2  10481  expnlbnd2  10645  shftlem  10824  resqrexlemgt0  11028  cau3lem  11122  clim2  11290  clim2c  11291  clim0c  11293  2clim  11308  climabs0  11314  climcn1  11315  climcn2  11316  climsqz  11342  climsqz2  11343  summodclem2  11389  fsum2dlemstep  11441  fsumiun  11484  mertenslem2  11543  mertensabs  11544  prodfrecap  11553  fprodeq0  11624  fprod2dlemstep  11629  gcdmultiplez  12021  dvdssq  12031  lcmgcdlem  12076  lcmdvds  12078  coprmdvds2  12092  pclemub  12286  pcge0  12311  pcgcd1  12326  prmpwdvds  12352  1arithlem4  12363  imasaddfnlemg  12734  imasaddflemg  12736  grpidpropdg  12792  grpridd  12805  mhmpropd  12856  mhmima  12874  grplcan  12931  dfgrp3mlem  12967  mulgdirlem  13012  subgmulg  13046  issubg4m  13051  subgintm  13056  ssnmz  13069  srglmhm  13174  srgrmhm  13175  ringpropd  13215  dvdsrpropdg  13314  islmod  13379  islmodd  13381  neipsm  13624  lmbrf  13685  lmss  13716  txbas  13728  txbasval  13737  tx1cn  13739  txlm  13749  isxmet2d  13818  elmopn2  13919  mopni3  13954  blsscls2  13963  metequiv2  13966  metss2lem  13967  metrest  13976  metcnp  13982  metcnp2  13983  metcnpi3  13987  elcncf2  14031  mulc1cncf  14046  cncfco  14048  cncfmet  14049  2sqlem9  14441