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  4480  wetrep  4481  fvun1  5743  f1elima  5946  caovimo  6248  supisoti  7301  prarloc  7818  reapmul1  8869  ltmul12a  9134  peano5uzti  9686  eluzp1m1  9878  lbzbi  9948  qreccl  9974  xrlttr  10128  xrltso  10129  elfzodifsumelfzo  10546  mertensabs  12223  ndvdsadd  12617  nn0seqcvgd  12738  isprm3  12815  ennnfonelemim  13175  prdsval  13486  grppropd  13730  ghmcmn  14044  neissex  15030  lgsval3  15891  gfsumval  16862