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

Theorem sylibd 148
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 143 . 2 (𝜑 → (𝜒𝜃))
41, 3syld 45 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3imtr3d  201  dvelimdf  1967  ceqsalt  2684  sbceqal  2934  csbiebt  3007  rspcsbela  3027  preqr1g  3661  repizf2  4054  copsexg  4134  onun2  4374  suc11g  4440  elrnrexdm  5525  isoselem  5687  riotass2  5722  oawordriexmid  6332  nnm00  6391  ecopovtrn  6492  ecopovtrng  6495  infglbti  6878  difinfsnlem  6950  enq0tr  7206  addnqprl  7301  addnqpru  7302  mulnqprl  7340  mulnqpru  7341  recexprlemss1l  7407  recexprlemss1u  7408  cauappcvgprlemdisj  7423  mulextsr1lem  7552  pitonn  7620  rereceu  7661  cnegexlem1  7901  ltadd2  8145  eqord2  8210  mulext  8339  mulgt1  8581  lt2halves  8909  addltmul  8910  nzadd  9060  zextlt  9097  recnz  9098  zeo  9110  peano5uzti  9113  irradd  9390  irrmul  9391  xltneg  9570  xleadd1  9609  icc0r  9660  fznuz  9833  uznfz  9834  facndiv  10436  rennim  10725  abs00ap  10785  absle  10812  cau3lem  10837  caubnd2  10840  climshft  11024  subcn2  11031  mulcn2  11032  serf0  11072  cvgratnnlemnexp  11244  cvgratnnlemmn  11245  efieq1re  11387  moddvds  11409  dvdsssfz1  11457  nn0seqcvgd  11629  algcvgblem  11637  eucalglt  11645  lcmgcdlem  11665  rpmul  11686  divgcdcoprm0  11689  isprm6  11732  rpexp  11738  tgss3  12153  cnpnei  12294  cnntr  12300  hmeoopn  12386  hmeocld  12387  mulcncflem  12665  bj-peano4  12987
  Copyright terms: Public domain W3C validator