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

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

Proof of Theorem sylancr
StepHypRef Expression
1 sylancr.1 . . 3 ψ
21a1i 10 . 2 (φψ)
3 sylancr.2 . 2 (φχ)
4 sylancr.3 . 2 ((ψ χ) → θ)
52, 3, 4syl2anc 642 1 (φθ)
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358
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  df-an 360
This theorem is referenced by:  unipw  4117  imakexg  4299  pwexg  4328  snfi  4431  1cspfin  4543  vfintle  4546  vfin1cltv  4547  phialllem2  4617  coexg  4749  ov  5595  mpteq2da  5666  brcupg  5814  brcomposeg  5819  brcrossg  5848  frds  5935  qsexg  5982  enmap2lem5  6067  enmap1lem5  6073  enprmaplem6  6081  enpw  6087  dflec2  6210  nmembers1lem3  6270  nchoicelem19  6307  frecexg  6312  dmfrec  6316  fnfreclem1  6317  fnfreclem2  6318  fnfreclem3  6319  frec0  6321  frecsuc  6322
  Copyright terms: Public domain W3C validator