Theorem anasss 397

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 362	. 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  399  anabss3  580  wepo  4342  wetrep  4343  fvun1  5560  f1elima  5749  caovimo  6043  supisoti  6983  prarloc  7452  reapmul1  8501  ltmul12a  8763  peano5uzti  9307  eluzp1m1  9497  lbzbi  9562  qreccl  9588  xrlttr  9739  xrltso  9740  elfzodifsumelfzo  10144  mertensabs  11487  ndvdsadd  11877  nn0seqcvgd  11982  isprm3  12059  ennnfonelemim  12366  grppropd  12711  neissex  12918  lgsval3  13672