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

Theorem anasss 385
 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 350 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 248 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem is referenced by:  anass  387  anabss3  527  wepo  4124  wetrep  4125  fvun1  5267  f1elima  5440  caovimo  5722  supisoti  6414  prarloc  6659  reapmul1  7660  ltmul12a  7901  peano5uzti  8405  eluzp1m1  8592  lbzbi  8648  qreccl  8674  xrlttr  8817  xrltso  8818  elfzodifsumelfzo  9159  ndvdsadd  10243  nn0seqcvgd  10263
 Copyright terms: Public domain W3C validator