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  wepo  4359  wetrep  4360  fvun1  5582  f1elima  5773  caovimo  6067  supisoti  7008  prarloc  7501  reapmul1  8551  ltmul12a  8816  peano5uzti  9360  eluzp1m1  9550  lbzbi  9615  qreccl  9641  xrlttr  9794  xrltso  9795  elfzodifsumelfzo  10200  mertensabs  11544  ndvdsadd  11935  nn0seqcvgd  12040  isprm3  12117  ennnfonelemim  12424  grppropd  12892  neissex  13635  lgsval3  14389