NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  syl5ibcom GIF version

Theorem syl5ibcom 211
Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)
Hypotheses
Ref Expression
syl5ib.1 (φψ)
syl5ib.2 (χ → (ψθ))
Assertion
Ref Expression
syl5ibcom (φ → (χθ))

Proof of Theorem syl5ibcom
StepHypRef Expression
1 syl5ib.1 . . 3 (φψ)
2 syl5ib.2 . . 3 (χ → (ψθ))
31, 2syl5ib 210 . 2 (χ → (φθ))
43com12 27 1 (φ → (χθ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  biimpcd  215  mob2  3016  rmob  3134  ltfintri  4466  ncfineleq  4477  tfinltfin  4501  tfinnn  4534  sfinltfin  4535  vfinncvntnn  4548  vfinspsslem1  4550  phi11lem1  4595  phialllem1  4616  xp11  5056  tz6.12c  5347  weds  5938  erth  5968  ectocld  5991  ecoptocl  5996  mapsn  6026  fndmeng  6046  enmap1lem3  6071  enprmaplem6  6081  ltlenlec  6207  nchoicelem9  6297
  Copyright terms: Public domain W3C validator