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  580  annimdc  845  dn1dc  867  xordidc  1290  nfimd  1477  exlimd2  1486  elex22  2569  elex2  2570  spcimdv  2637  spcimedv  2639  spsbcd  2776  opth  3974  euotd  3991  ssorduni  4213  wetriext  4301  tfisi  4310  sotri2  4722  sotri3  4723  unielrel  4845  funmo  4917  fnfvima  5393  fliftfun  5436  fliftval  5440  riota5f  5492  riotass2  5494  grprinvlem  5695  grprinvd  5696  caofref  5732  tfrlem1  5923  tfrlem5  5930  tfrlemibxssdm  5941  tfrlemibfn  5942  tfrlemiex  5945  rdgisucinc  5972  frecabex  5984  ertr  6121  qliftlem  6184  th3q  6211  f1dom2g  6236  dom3d  6254  en1  6279  xpdom3m  6308  phplem4dom  6324  phpm  6327  phpelm  6328  findcard  6345  ordiso2  6355  recexnq  6486  ltbtwnnqq  6511  addnnnq0  6545  mulnnnq0  6546  prltlu  6583  prarloclemn  6595  prarloc  6599  distrlem1prl  6678  distrlem1pru  6679  distrlem4prl  6680  distrlem4pru  6681  ltexprlemrl  6706  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  caucvgprprlemml  6790  addsrpr  6828  mulsrpr  6829  axcaucvglemres  6971  lemul12a  7826  lemulge11  7830  nngt0  7937  nn0ge0  8205  nn0ge2m1nn  8240  zletric  8287  zlelttric  8288  nn0n0n1ge2b  8318  nn0ind-raph  8353  rpge0  8593  fz0fzelfz0  8982  fz0fzdiffz0  8985  ige2m2fzo  9052  elfzodifsumelfzo  9055  elfzom1elp1fzo  9056  qletric  9097  qlelttric  9098  qbtwnzlemshrink  9102  rebtwn2zlemshrink  9106  frecuzrdgfn  9172  frecuzrdg0  9174  frecfzennn  9177  iseqovex  9193  iseqfn  9195  iseq1  9196  iseqcl  9197  iseqp1  9199  iseqfveq2  9202  iseqfveq  9204  iseqshft2  9206  monoord  9209  monoord2  9210  isermono  9211  iseqsplit  9212  iseqcaopr3  9214  iseqid3s  9220  iseqid  9221  iseqhomo  9222  expcl2lemap  9241  leexp1a  9283  expnbnd  9346  cvg1nlemcau  9557  cvg1nlemres  9558  recvguniq  9567  resqrexlemdecn  9584  resqrexlemgt0  9592  resqrexlemoverl  9593  resqrexlemglsq  9594  cau3lem  9684  climi  9782  climcn1  9803  climcn2  9804  ialgfx  9865