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  6477  genpcdl  6502  genpcuu  6503  mulnqprl  6549  mulnqpru  6550  distrlem1prl  6558  distrlem1pru  6559  distrlem4prl  6560  distrlem4pru  6561  distrlem5prl  6562  distrlem5pru  6563  ltsopr  6570  ltexprlemfl  6583  ltexprlemfu  6585  recexprlemss1l  6607  recexprlemss1u  6608  aptiprleml  6611  ltsrprg  6675  lttrsr  6690  mulextsr1lem  6706  axapti  6887  cnegexlem1  6983  le2add  7234  lt2add  7235  ltleadd  7236  lt2sub  7250  le2sub  7251  recexre  7362  reapti  7363  apreap  7371  reapcotr  7382  remulext1  7383  apreim  7387  apcotr  7391  mulext2  7397  recexap  7416  addltmul  7938  elnnz  8031  zleloe  8068  nn0n0n1ge2b  8096  nn0lt2  8098  zextlt  8108  uzind2  8126  eluzdc  8323  qreccl  8351  xltnegi  8518  iccid  8564  icoshft  8628  fzofzim  8814  frec2uzrand  8872  frecuzrdgfn  8879  absnid  9227
  Copyright terms: Public domain W3C validator