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  393  jc  567  annimdc  831  dn1dc  853  xordidc  1271  nfimd  1455  exlimd2  1464  elex22  2542  elex2  2543  spcimdv  2610  spcimedv  2612  spsbcd  2749  opth  3944  euotd  3961  ssorduni  4159  tfisi  4233  sotri2  4645  sotri3  4646  unielrel  4768  funmo  4839  fnfvima  5314  fliftfun  5357  fliftval  5361  riota5f  5412  riotass2  5414  grprinvlem  5614  grprinvd  5615  caofref  5651  tfrlem1  5841  tfrlem5  5848  tfrlemibxssdm  5858  tfrlemibfn  5859  tfrlemiex  5862  rdgisucinc  5888  ertr  6028  qliftlem  6091  th3q  6118  recex  6243  ltbtwnnqq  6266  addnnnq0  6298  mulnnnq0  6299  prltlu  6335  prarloclemn  6347  prarloc  6351  distrlem1prl  6415  distrlem1pru  6416  distrlem4prl  6417  distrlem4pru  6418  ltexprlemrl  6441  addsrpr  6489  mulsrpr  6490