Theorem anasss 396

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 361	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 255	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  anass  398  anabss3  574  wepo  4281  wetrep  4282  fvun1  5487  f1elima  5674  caovimo  5964  supisoti  6897  prarloc  7311  reapmul1  8357  ltmul12a  8618  peano5uzti  9159  eluzp1m1  9349  lbzbi  9408  qreccl  9434  xrlttr  9581  xrltso  9582  elfzodifsumelfzo  9978  mertensabs  11306  ndvdsadd  11628  nn0seqcvgd  11722  isprm3  11799  ennnfonelemim  11937  neissex  12334