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  4482  wetrep  4483  fvun1  5745  f1elima  5948  caovimo  6250  supisoti  7303  prarloc  7820  reapmul1  8871  ltmul12a  9136  peano5uzti  9689  eluzp1m1  9881  lbzbi  9951  qreccl  9977  xrlttr  10131  xrltso  10132  elfzodifsumelfzo  10550  mertensabs  12227  ndvdsadd  12621  nn0seqcvgd  12742  isprm3  12819  ennnfonelemim  13192  prdsval  13503  grppropd  13747  ghmcmn  14061  neissex  15047  lgsval3  15908  gfsumval  16879