Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylibd GIF 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  1892  ceqsalt  2580  sbceqal  2814  sbcimdv  2823  csbiebt  2886  rspcsbela  2905  preqr1g  3537  repizf2  3915  copsexg  3981  onun2  4216  suc11g  4281  elrnrexdm  5306  isoselem  5459  riotass2  5494  nnm00  6102  ecopovtrn  6203  ecopovtrng  6206  enq0tr  6532  addnqprl  6627  addnqpru  6628  mulnqprl  6666  mulnqpru  6667  recexprlemss1l  6733  recexprlemss1u  6734  cauappcvgprlemdisj  6749  mulextsr1lem  6864  pitonn  6924  rereceu  6963  cnegexlem1  7186  ltadd2  7416  mulext  7605  mulgt1  7829  lt2halves  8160  addltmul  8161  zextlt  8332  recnz  8333  zeo  8343  peano5uzti  8346  irradd  8580  irrmul  8581  xltneg  8749  icc0r  8795  fznuz  8964  uznfz  8965  rennim  9600  abs00ap  9660  absle  9685  cau3lem  9710  caubnd2  9713  climshft  9825  subcn2  9832  mulcn2  9833  serif0  9871  nn0seqcvgd  9880  algcvgblem  9888  bj-peano4  10080
 Copyright terms: Public domain W3C validator