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

Theorem sylc 56
Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)
Hypotheses
Ref Expression
sylc.1 (φψ)
sylc.2 (φχ)
sylc.3 (ψ → (χθ))
Assertion
Ref Expression
sylc (φθ)

Proof of Theorem sylc
StepHypRef Expression
1 sylc.1 . . 3 (φψ)
2 sylc.2 . . 3 (φχ)
3 sylc.3 . . 3 (ψ → (χθ))
41, 2, 3syl2im 34 . 2 (φ → (φθ))
54pm2.43i 43 1 (φθ)
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl3c  57  mpsyl  59  jc  139  2thd  231  jca  518  syl2anc  642  nfimd  1808  ax12  1935  ax12from12o  2156  equid1  2158  elex22  2870  elex2  2871  spcimdv  2936  spsbcd  3059  nnceleq  4430  tfinltfin  4501  sfinltfin  4535  sfin111  4536  phialllem1  4616  fvopab4t  5385  fvelrn  5413  frd  5922  refd  5927  enadjlem1  6059  enadj  6060  enprmaplem3  6078  1cnc  6139
  Copyright terms: Public domain W3C validator