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  587  biadanid  618  wepo  4456  wetrep  4457  fvun1  5712  f1elima  5913  caovimo  6215  supisoti  7208  prarloc  7722  reapmul1  8774  ltmul12a  9039  peano5uzti  9587  eluzp1m1  9779  lbzbi  9849  qreccl  9875  xrlttr  10029  xrltso  10030  elfzodifsumelfzo  10445  mertensabs  12097  ndvdsadd  12491  nn0seqcvgd  12612  isprm3  12689  ennnfonelemim  13044  prdsval  13355  grppropd  13599  ghmcmn  13913  neissex  14888  lgsval3  15746  gfsumval  16680