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

Theorem sylbid 206
 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 198 . 2 (φ → (ψχ))
3 sylbid.2 . 2 (φ → (χθ))
42, 3syld 40 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:  3imtr4d  259  ax11eq  2193  ax11el  2194  leltfintr  4458  tfin11  4493  sfinltfin  4535  phi11lem1  4595  xp11  5056  xpcan  5057  xpcan2  5058  enprmaplem3  6078  enprmaplem6  6081  ce0addcnnul  6179  ceclb  6183  fce  6188  sbth  6206  dflec2  6210  lectr  6211  leaddc1  6214  leconnnc  6218  tlecg  6230  letc  6231  ce0lenc1  6239  nclenn  6249  lemuc1  6253  lecadd2  6266  ncslesuc  6267  nchoicelem9  6297  nchoicelem12  6300  nchoicelem17  6305  dmfrec  6316  fnfreclem2  6318  fnfreclem3  6319
 Copyright terms: Public domain W3C validator