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  biadanid  616  wepo  4449  wetrep  4450  fvun1  5699  f1elima  5896  caovimo  6198  supisoti  7173  prarloc  7686  reapmul1  8738  ltmul12a  9003  peano5uzti  9551  eluzp1m1  9742  lbzbi  9807  qreccl  9833  xrlttr  9987  xrltso  9988  elfzodifsumelfzo  10402  mertensabs  12043  ndvdsadd  12437  nn0seqcvgd  12558  isprm3  12635  ennnfonelemim  12990  prdsval  13301  grppropd  13545  ghmcmn  13859  neissex  14833  lgsval3  15691