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  4377  wetrep  4378  fvun1  5603  f1elima  5795  caovimo  6090  supisoti  7039  prarloc  7532  reapmul1  8582  ltmul12a  8847  peano5uzti  9391  eluzp1m1  9581  lbzbi  9646  qreccl  9672  xrlttr  9825  xrltso  9826  elfzodifsumelfzo  10231  mertensabs  11577  ndvdsadd  11968  nn0seqcvgd  12073  isprm3  12150  ennnfonelemim  12475  grppropd  12962  ghmcmn  13265  neissex  14122  lgsval3  14877