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  614  wepo  4391  wetrep  4392  fvun1  5624  f1elima  5817  caovimo  6114  supisoti  7071  prarloc  7565  reapmul1  8616  ltmul12a  8881  peano5uzti  9428  eluzp1m1  9619  lbzbi  9684  qreccl  9710  xrlttr  9864  xrltso  9865  elfzodifsumelfzo  10271  mertensabs  11683  ndvdsadd  12075  nn0seqcvgd  12182  isprm3  12259  ennnfonelemim  12584  grppropd  13092  ghmcmn  13400  neissex  14344  lgsval3  15175