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  4395  wetrep  4396  fvun1  5630  f1elima  5823  caovimo  6121  supisoti  7085  prarloc  7589  reapmul1  8641  ltmul12a  8906  peano5uzti  9453  eluzp1m1  9644  lbzbi  9709  qreccl  9735  xrlttr  9889  xrltso  9890  elfzodifsumelfzo  10296  mertensabs  11721  ndvdsadd  12115  nn0seqcvgd  12236  isprm3  12313  ennnfonelemim  12668  prdsval  12977  grppropd  13221  ghmcmn  13535  neissex  14509  lgsval3  15367