ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylbid 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  4290  poltletr  4725  xp11m  4759  fvmptdf  5258  eusvobj2  5498  ovmpt2df  5632  f1o2ndf1  5849  smoiso  5917  nnsseleq  6079  ecopovtrn  6203  ecopovtrng  6206  dom2lem  6252  fundmen  6286  fidifsnen  6331  findcard2  6346  findcard2s  6347  ordiso2  6355  addcanpig  6430  mulcanpig  6431  addnidpig  6432  ordpipqqs  6470  ltexnqq  6504  prarloclemlo  6590  genpcdl  6615  genpcuu  6616  mulnqprl  6664  mulnqpru  6665  distrlem1prl  6678  distrlem1pru  6679  distrlem4prl  6680  distrlem4pru  6681  distrlem5prl  6682  distrlem5pru  6683  ltsopr  6692  ltexprlemfl  6705  ltexprlemfu  6707  recexprlemss1l  6731  recexprlemss1u  6732  aptiprleml  6735  ltsrprg  6830  lttrsr  6845  mulextsr1lem  6862  axapti  7088  cnegexlem1  7184  le2add  7437  lt2add  7438  ltleadd  7439  lt2sub  7453  le2sub  7454  recexre  7567  reapti  7568  apreap  7576  reapcotr  7587  remulext1  7588  apreim  7592  apcotr  7596  mulext2  7602  recexap  7632  addltmul  8159  elnnz  8253  zleloe  8290  nn0n0n1ge2b  8318  nn0lt2  8320  zextlt  8330  uzind2  8348  eluzdc  8545  qreccl  8574  xltnegi  8746  iccid  8792  icoshft  8856  fzofzim  9042  flqeqceilz  9158  frec2uzrand  9189  frecuzrdgfn  9196  recvguniq  9591  abs00ap  9658  absext  9659  absnid  9669  cau3lem  9708  climuni  9812  2clim  9820  algcvgblem  9886  ialgcvga  9888
  Copyright terms: Public domain W3C validator