ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylibd Structured version   Unicode version

Theorem sylibd 138
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylibd.1
sylibd.2
Assertion
Ref Expression
sylibd

Proof of Theorem sylibd
StepHypRef Expression
1 sylibd.1 . 2
2 sylibd.2 . . 3
32biimpd 132 . 2
41, 3syld 40 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3imtr3d  191  dvelimdf  1889  ceqsalt  2574  sbceqal  2808  sbcimdv  2817  csbiebt  2880  rspcsbela  2899  preqr1g  3528  repizf2  3906  copsexg  3972  onun2  4182  suc11g  4235  elrnrexdm  5249  isoselem  5402  riotass2  5437  nnm00  6038  ecopovtrn  6139  ecopovtrng  6142  enq0tr  6416  addnqprl  6511  addnqpru  6512  mulnqprl  6548  mulnqpru  6549  recexprlemss1l  6606  recexprlemss1u  6607  cauappcvgprlemdisj  6622  mulextsr1lem  6686  pitonn  6724  cnegexlem1  6963  ltadd2  7192  mulext  7378  mulgt1  7590  lt2halves  7917  addltmul  7918  zextlt  8088  recnz  8089  zeo  8099  peano5uzti  8102  irradd  8335  irrmul  8336  xltneg  8499  icc0r  8545  fznuz  8714  uznfz  8715  rennim  9191  bj-peano4  9389
  Copyright terms: Public domain W3C validator