ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylibd Structured version   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  1874  ceqsalt  2557  sbceqal  2791  sbcimdv  2800  csbiebt  2863  rspcsbela  2882  preqr1g  3511  repizf2  3889  copsexg  3955  onun2  4166  suc11g  4219  elrnrexdm  5231  isoselem  5384  riotass2  5418  nnm00  6013  ecopovtrn  6114  ecopovtrng  6117  enq0tr  6289  addnqprl  6384  addnqpru  6385  mulnqprl  6412  mulnqpru  6413  recexprlemss1l  6469  recexprlemss1u  6470  cnegexlem1  6773  bj-peano4  7177
  Copyright terms: Public domain W3C validator