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  6432  mulnnnq0  6433  prltlu  6470  prarloclemn  6482  prarloc  6486  distrlem1prl  6558  distrlem1pru  6559  distrlem4prl  6560  distrlem4pru  6561  ltexprlemrl  6584  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  addsrpr  6673  mulsrpr  6674  lemul12a  7609  lemulge11  7613  nngt0  7720  nn0ge0  7983  nn0ge2m1nn  8018  zletric  8065  zlelttric  8066  nn0n0n1ge2b  8096  nn0ind-raph  8131  rpge0  8370  fz0fzelfz0  8754  fz0fzdiffz0  8757  ige2m2fzo  8824  elfzodifsumelfzo  8827  elfzom1elp1fzo  8828  frecuzrdgfn  8879  frecuzrdg0  8881  frecfzennn  8884  iseqovex  8899  iseqfn  8901  iseq1  8902  iseqcl  8903  iseqp1  8904  iseqfveq2  8905  iseqfveq  8907  expcl2lemap  8921  leexp1a  8963  expnbnd  9025