Theorem anasss 403

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

Hypothesis

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

Assertion

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

Proof of Theorem anasss

Step	Hyp	Ref	Expression
1		anasss.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
2	1	exp31 364	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 257	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  anass  405  anabss3  591  biadanid  622  wepo  4504  wetrep  4505  fvun1  5769  f1elima  5979  caovimo  6283  supisoti  7351  prarloc  7871  reapmul1  8926  ltmul12a  9193  peano5uzti  9759  eluzp1m1  9956  lbzbi  10026  qreccl  10052  xrlttr  10208  xrltso  10209  elfzodifsumelfzo  10630  mertensabs  12323  ndvdsadd  12717  nn0seqcvgd  12838  isprm3  12915  ennnfonelemim  13367  grppropd  13875  ghmcmn  14215  gsumvalfi  14236  prdsval  14257  neissex  15357  lgsval3  16303