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  5914  caovimo  6216  supisoti  7209  prarloc  7723  reapmul1  8775  ltmul12a  9040  peano5uzti  9588  eluzp1m1  9780  lbzbi  9850  qreccl  9876  xrlttr  10030  xrltso  10031  elfzodifsumelfzo  10447  mertensabs  12103  ndvdsadd  12497  nn0seqcvgd  12618  isprm3  12695  ennnfonelemim  13050  prdsval  13361  grppropd  13605  ghmcmn  13919  neissex  14895  lgsval3  15753  gfsumval  16707