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

Theorem syl6bi 219
 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 198 . 2 (φ → (ψχ))
3 syl6bi.2 . 2 (χθ)
42, 3syl6 29 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:  ax11i  1647  equveli  1988  eupickbi  2270  2eu2  2285  rgen2a  2680  reu6  3025  sseq0  3582  disjel  3597  disjpss  3601  uneqdifeq  3638  elinti  3935  pwadjoin  4119  preq12b  4127  nnsucelr  4428  sfindbl  4530  funimass2  5170  fconstfv  5456  oprabid  5550  enadj  6060  enpw1  6062  enprmaplem3  6078  nenpw1pwlem2  6085  1cnc  6139  ncspw1eu  6159  ce0nnulb  6182  letc  6231  ncslesuc  6267  nchoicelem3  6291  fnfreclem2  6318  fnfreclem3  6319
 Copyright terms: Public domain W3C validator