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

Step	Hyp	Ref	Expression
1		sylc.1	. . 3 ⊢ (φ → ψ)
2		sylc.2	. . 3 ⊢ (φ → χ)
3		sylc.3	. . 3 ⊢ (ψ → (χ → θ))
4	1, 2, 3	syl2im 34	. 2 ⊢ (φ → (φ → θ))
5	4	pm2.43i 43	1 ⊢ (φ → θ)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  syl3c  57  mpsyl  59  imp  115  2thd  164  jca  290  syl2anc  391  jc  579  annimdc  844  dn1dc  866  xordidc  1287  nfimd  1474  exlimd2  1483  elex22  2563  elex2  2564  spcimdv  2631  spcimedv  2633  spsbcd  2770  opth  3965  euotd  3982  ssorduni  4179  tfisi  4253  sotri2  4665  sotri3  4666  unielrel  4788  funmo  4860  fnfvima  5336  fliftfun  5379  fliftval  5383  riota5f  5435  riotass2  5437  grprinvlem  5637  grprinvd  5638  caofref  5674  tfrlem1  5864  tfrlem5  5871  tfrlemibxssdm  5882  tfrlemibfn  5883  tfrlemiex  5886  rdgisucinc  5912  frecabex  5923  ertr  6057  qliftlem  6120  th3q  6147  f1dom2g  6172  dom3d  6190  en1  6215  xpdom3m  6244  recexnq  6374  ltbtwnnqq  6398  addnnnq0  6431  mulnnnq0  6432  prltlu  6469  prarloclemn  6481  prarloc  6485  distrlem1prl  6556  distrlem1pru  6557  distrlem4prl  6558  distrlem4pru  6559  ltexprlemrl  6582  addsrpr  6633  mulsrpr  6634  lemul12a  7569  lemulge11  7573  nngt0  7680  nn0ge0  7943  nn0ge2m1nn  7978  zletric  8025  zlelttric  8026  nn0n0n1ge2b  8056  nn0ind-raph  8091  rpge0  8330  fz0fzelfz0  8714  fz0fzdiffz0  8717  ige2m2fzo  8784  elfzodifsumelfzo  8787  elfzom1elp1fzo  8788  frecuzrdgfn  8839  frecuzrdg0  8841  frecfzennn  8844  iseqovex  8859  iseqfn  8861  iseq1  8862  iseqcl  8863  iseqp1  8864  iseqfveq2  8865  iseqfveq  8867  expcl2lemap  8881  leexp1a  8923  expnbnd  8985