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  587  biadanid  618  wepo  4462  wetrep  4463  fvun1  5721  f1elima  5924  caovimo  6226  supisoti  7252  prarloc  7766  reapmul1  8817  ltmul12a  9082  peano5uzti  9632  eluzp1m1  9824  lbzbi  9894  qreccl  9920  xrlttr  10074  xrltso  10075  elfzodifsumelfzo  10492  mertensabs  12161  ndvdsadd  12555  nn0seqcvgd  12676  isprm3  12753  ennnfonelemim  13108  prdsval  13419  grppropd  13663  ghmcmn  13977  neissex  14959  lgsval3  15820  gfsumval  16792