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  4450  wetrep  4451  fvun1  5702  f1elima  5903  caovimo  6205  supisoti  7188  prarloc  7701  reapmul1  8753  ltmul12a  9018  peano5uzti  9566  eluzp1m1  9758  lbzbi  9823  qreccl  9849  xrlttr  10003  xrltso  10004  elfzodifsumelfzo  10419  mertensabs  12063  ndvdsadd  12457  nn0seqcvgd  12578  isprm3  12655  ennnfonelemim  13010  prdsval  13321  grppropd  13565  ghmcmn  13879  neissex  14854  lgsval3  15712