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

Theorem sylbid 139
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylbid.1 (φ → (ψχ))
sylbid.2 (φ → (χθ))
Assertion
Ref Expression
sylbid (φ → (ψθ))

Proof of Theorem sylbid
StepHypRef Expression
1 sylbid.1 . . 3 (φ → (ψχ))
21biimpd 132 . 2 (φ → (ψχ))
3 sylbid.2 . 2 (φ → (χθ))
42, 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:  3imtr4d  192  nlimsucg  4242  poltletr  4668  xp11m  4702  fvmptdf  5201  eusvobj2  5441  ovmpt2df  5574  f1o2ndf1  5791  smoiso  5858  ecopovtrn  6139  ecopovtrng  6142  dom2lem  6188  fundmen  6222  addcanpig  6318  mulcanpig  6319  addnidpig  6320  ordpipqqs  6358  ltexnqq  6391  prarloclemlo  6476  genpcdl  6501  genpcuu  6502  mulnqprl  6548  mulnqpru  6549  distrlem1prl  6557  distrlem1pru  6558  distrlem4prl  6559  distrlem4pru  6560  distrlem5prl  6561  distrlem5pru  6562  ltsopr  6569  ltexprlemfl  6582  ltexprlemfu  6584  recexprlemss1l  6606  recexprlemss1u  6607  aptiprleml  6610  ltsrprg  6655  lttrsr  6670  mulextsr1lem  6686  axapti  6867  cnegexlem1  6963  le2add  7214  lt2add  7215  ltleadd  7216  lt2sub  7230  le2sub  7231  recexre  7342  reapti  7343  apreap  7351  reapcotr  7362  remulext1  7363  apreim  7367  apcotr  7371  mulext2  7377  recexap  7396  addltmul  7918  elnnz  8011  zleloe  8048  nn0n0n1ge2b  8076  nn0lt2  8078  zextlt  8088  uzind2  8106  eluzdc  8303  qreccl  8331  xltnegi  8498  iccid  8544  icoshft  8608  fzofzim  8794  frec2uzrand  8852  frecuzrdgfn  8859  absnid  9207
  Copyright terms: Public domain W3C validator