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

Theorem syl6bi 152
Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)
Hypotheses
Ref Expression
syl6bi.1 (φ → (ψχ))
syl6bi.2 (χθ)
Assertion
Ref Expression
syl6bi (φ → (ψθ))

Proof of Theorem syl6bi
StepHypRef Expression
1 syl6bi.1 . . 3 (φ → (ψχ))
21biimpd 132 . 2 (φ → (ψχ))
3 syl6bi.2 . 2 (χθ)
42, 3syl6 29 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:  19.33bdc  1518  ax11i  1599  equveli  1639  eupickbi  1979  rgen2a  2369  reu6  2724  sseq0  3252  disjel  3268  disjpss  3272  preq12b  3532  prel12  3533  prneimg  3536  elinti  3615  opthreg  4234  elreldm  4503  issref  4650  relcnvtr  4783  relresfld  4790  funopg  4877  funimass2  4920  fvimacnv  5225  elunirn  5348  oprabid  5480  op1steq  5747  f1o2ndf1  5791  reldmtpos  5809  rntpos  5813  nntri3or  6011  nnaordex  6036  nnawordex  6037  lt2addnq  6388  genpelvl  6494  genpelvu  6495  distrlem5prl  6561  distrlem5pru  6562  ltxrlt  6862  0mnnnnn0  7970  elnnnn0b  7982  btwnz  8113  uz11  8251  nn01to3  8308  zq  8317  xrltso  8467  xltnegi  8498  iccleub  8550  fzdcel  8654  uznfz  8715  2ffzeq  8748  elfzonlteqm1  8816  frecuzrdgfn  8859  fzfig  8867  bj-elssuniab  9245  bj-nn0sucALT  9408
  Copyright terms: Public domain W3C validator