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  4485  wetrep  4486  fvun1  5748  f1elima  5952  caovimo  6256  supisoti  7314  prarloc  7834  reapmul1  8886  ltmul12a  9151  peano5uzti  9704  eluzp1m1  9896  lbzbi  9966  qreccl  9992  xrlttr  10147  xrltso  10148  elfzodifsumelfzo  10568  mertensabs  12248  ndvdsadd  12642  nn0seqcvgd  12763  isprm3  12840  ennnfonelemim  13259  grppropd  13772  ghmcmn  14080  gfsumval  14102  prdsval  14115  neissex  15156  lgsval3  16017