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  wepo  4360  wetrep  4361  fvun1  5583  f1elima  5774  caovimo  6068  supisoti  7009  prarloc  7502  reapmul1  8552  ltmul12a  8817  peano5uzti  9361  eluzp1m1  9551  lbzbi  9616  qreccl  9642  xrlttr  9795  xrltso  9796  elfzodifsumelfzo  10201  mertensabs  11545  ndvdsadd  11936  nn0seqcvgd  12041  isprm3  12118  ennnfonelemim  12425  grppropd  12893  neissex  13668  lgsval3  14422