Theorem anasss 399

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 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

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  anabss3  585  biadanid  614  wepo  4414  wetrep  4415  fvun1  5658  f1elima  5855  caovimo  6153  supisoti  7127  prarloc  7636  reapmul1  8688  ltmul12a  8953  peano5uzti  9501  eluzp1m1  9692  lbzbi  9757  qreccl  9783  xrlttr  9937  xrltso  9938  elfzodifsumelfzo  10352  mertensabs  11923  ndvdsadd  12317  nn0seqcvgd  12438  isprm3  12515  ennnfonelemim  12870  prdsval  13180  grppropd  13424  ghmcmn  13738  neissex  14712  lgsval3  15570