Theorem anasss 392

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  anass  394  anabss3  553  wepo  4195  wetrep  4196  fvun1  5383  f1elima  5566  caovimo  5852  supisoti  6759  prarloc  7123  reapmul1  8133  ltmul12a  8382  peano5uzti  8915  eluzp1m1  9103  lbzbi  9162  qreccl  9188  xrlttr  9326  xrltso  9327  elfzodifsumelfzo  9673  mertensabs  10992  ndvdsadd  11270  nn0seqcvgd  11362  isprm3  11439