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

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
StepHypRef Expression
1 anasss.1 . . 3 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
21exp31 364 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 257 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff set class
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  biadanid  614  wepo  4377  wetrep  4378  fvun1  5603  f1elima  5795  caovimo  6090  supisoti  7039  prarloc  7532  reapmul1  8582  ltmul12a  8847  peano5uzti  9391  eluzp1m1  9581  lbzbi  9646  qreccl  9672  xrlttr  9825  xrltso  9826  elfzodifsumelfzo  10231  mertensabs  11577  ndvdsadd  11968  nn0seqcvgd  12073  isprm3  12150  ennnfonelemim  12475  grppropd  12962  ghmcmn  13265  neissex  14122  lgsval3  14877
  Copyright terms: Public domain W3C validator