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  4454  wetrep  4455  fvun1  5708  f1elima  5909  caovimo  6211  supisoti  7200  prarloc  7713  reapmul1  8765  ltmul12a  9030  peano5uzti  9578  eluzp1m1  9770  lbzbi  9840  qreccl  9866  xrlttr  10020  xrltso  10021  elfzodifsumelfzo  10436  mertensabs  12088  ndvdsadd  12482  nn0seqcvgd  12603  isprm3  12680  ennnfonelemim  13035  prdsval  13346  grppropd  13590  ghmcmn  13904  neissex  14879  lgsval3  15737