Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  anasss GIF version

Theorem anasss 396
 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
StepHypRef Expression
1 anasss.1 . . 3 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
21exp31 361 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 255 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem is referenced by:  anass  398  anabss3  574  wepo  4281  wetrep  4282  fvun1  5487  f1elima  5674  caovimo  5964  supisoti  6897  prarloc  7318  reapmul1  8364  ltmul12a  8625  peano5uzti  9166  eluzp1m1  9356  lbzbi  9415  qreccl  9441  xrlttr  9588  xrltso  9589  elfzodifsumelfzo  9985  mertensabs  11313  ndvdsadd  11635  nn0seqcvgd  11729  isprm3  11806  ennnfonelemim  11944  neissex  12344
 Copyright terms: Public domain W3C validator