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

Theorem sylancl 643
Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
sylancl.1 (φψ)
sylancl.2 χ
sylancl.3 ((ψ χ) → θ)
Assertion
Ref Expression
sylancl (φθ)

Proof of Theorem sylancl
StepHypRef Expression
1 sylancl.1 . 2 (φψ)
2 sylancl.2 . . 3 χ
32a1i 10 . 2 (φχ)
4 sylancl.3 . 2 ((ψ χ) → θ)
51, 3, 4syl2anc 642 1 (φθ)
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358
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  df-an 360
This theorem is referenced by:  equveli  1988  syl5sseq  3319  ssdifin0  3631  uneqdifeq  3638  unimax  3925  pw1exg  4302  cokexg  4309  pwexg  4328  nnsucelr  4428  vfinspnn  4541  isoini2  5498  fullfunexg  5859  qsexg  5982  mapsn  6026  enrflxg  6034  cnven  6045  ncdisjun  6136  addccan2nclem2  6264  nncdiv3  6277  nnc3n3p1  6278  nnc3n3p2  6279  nchoicelem1  6289  nchoicelem2  6290  nchoicelem12  6300  frec0  6321
  Copyright terms: Public domain W3C validator