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

Theorem anasss 392
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 357 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 254 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  anass  394  anabss3  553  wepo  4195  wetrep  4196  fvun1  5383  f1elima  5566  caovimo  5852  supisoti  6759  prarloc  7123  reapmul1  8133  ltmul12a  8382  peano5uzti  8915  eluzp1m1  9103  lbzbi  9162  qreccl  9188  xrlttr  9326  xrltso  9327  elfzodifsumelfzo  9673  mertensabs  10992  ndvdsadd  11270  nn0seqcvgd  11362  isprm3  11439
  Copyright terms: Public domain W3C validator