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

Theorem syl5ibr 212
 Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)
Hypotheses
Ref Expression
syl5ibr.1 (φθ)
syl5ibr.2 (χ → (ψθ))
Assertion
Ref Expression
syl5ibr (χ → (φψ))

Proof of Theorem syl5ibr
StepHypRef Expression
1 syl5ibr.1 . 2 (φθ)
2 syl5ibr.2 . . 3 (χ → (ψθ))
32bicomd 192 . 2 (χ → (θψ))
41, 3syl5ib 210 1 (χ → (φψ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  syl5ibrcom  213  biimprd  214  dvelimv  1939  pm2.61ne  2591  unineq  3505  sspw1  4335  vfinncvntnn  4548  ffvresb  5431  peano4nc  6150  ce0addcnnul  6179  ce0nn  6180  ceclb  6183  dflec2  6210  ce0lenc1  6239  addcdi  6250  nchoicelem17  6305  frecxp  6314
 Copyright terms: Public domain W3C validator