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

Theorem sylibd 142
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 136 . 2 (𝜑 → (𝜒𝜃))
41, 3syld 44 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  3imtr3d  195  dvelimdf  1906  ceqsalt  2595  sbceqal  2838  csbiebt  2911  rspcsbela  2930  preqr1g  3562  repizf2  3940  copsexg  4006  onun2  4241  suc11g  4306  elrnrexdm  5331  isoselem  5484  riotass2  5519  nnm00  6130  ecopovtrn  6231  ecopovtrng  6234  enq0tr  6560  addnqprl  6655  addnqpru  6656  mulnqprl  6694  mulnqpru  6695  recexprlemss1l  6761  recexprlemss1u  6762  cauappcvgprlemdisj  6777  mulextsr1lem  6892  pitonn  6952  rereceu  6991  cnegexlem1  7219  ltadd2  7458  mulext  7649  mulgt1  7874  lt2halves  8187  addltmul  8188  nzadd  8324  zextlt  8360  recnz  8361  zeo  8372  peano5uzti  8375  irradd  8648  irrmul  8649  xltneg  8820  icc0r  8866  fznuz  9036  uznfz  9037  facndiv  9571  rennim  9792  abs00ap  9852  absle  9879  cau3lem  9904  caubnd2  9907  climshft  10019  subcn2  10026  mulcn2  10027  serif0  10065  moddvds  10080  dvdsssfz1  10127  nn0seqcvgd  10206  algcvgblem  10214  bj-peano4  10410
  Copyright terms: Public domain W3C validator