Theorem sylc 62

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 38	. 2 ⊢ (𝜑 → (𝜑 → 𝜃))
5	4	pm2.43i 49	1 ⊢ (𝜑 → 𝜃)

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  63  mpsyl  65  imp  124  2thd  175  jca  306  syl2anc  411  jc  656  jcnd  658  annimdc  946  pm4.55dc  947  orandc  948  dn1dc  969  syl2an23an  1336  xordidc  1444  nfimd  1634  exlimd2  1644  elex22  2831  elex2  2832  spcimdv  2903  spcimedv  2905  spcedv  2908  rspcdva  2928  elabd  2965  spsbcd  3058  ifeqeqxdc  3673  opth  4358  euotd  4376  ssorduni  4614  tfisi  4714  omsinds  4749  nnpredcl  4750  sotri2  5165  sotri3  5166  unielrel  5295  funmo  5372  fnfvima  5926  resfvresima  5929  fliftfun  5975  fliftval  5979  riota5f  6038  riotass2  6040  fovcld  6166  oprssdmm  6378  funsssuppss  6471  tfrlem5  6558  tfrlemibxssdm  6571  tfrlemibfn  6572  tfrlemiex  6575  tfr1onlemsucfn  6584  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemex  6591  tfr1onlemres  6593  tfrcllemsucfn  6597  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemex  6604  tfrcllemres  6606  tfrcl  6608  rdgisucinc  6629  frecabex  6642  frecabcl  6643  nntr2  6749  ertr  6795  qliftlem  6860  th3q  6887  resixp  6981  f1dom2g  7008  dom3d  7026  domssr  7030  en1  7052  xpdom3m  7098  xpf1o  7110  phplem4dom  7129  phpm  7133  phpelm  7134  findcard  7158  finexdc  7173  fiintim  7204  fisseneq  7208  ssfirab  7210  opabfi  7213  f1dmvrnfibi  7224  iunfidisj  7226  fidcenumlemrk  7237  dcfi  7281  2omapfi  7284  suplub2ti  7305  supelti  7306  ordiso2  7339  caseinl  7395  caseinr  7396  djudom  7397  difinfsn  7404  difinfinf  7405  ctm  7413  enumct  7419  nnnninfeq  7432  ismkvnex  7459  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  acfun  7527  exmidontriimlem2  7542  exmidontriimlem3  7543  exmidapne  7590  cc2lem  7596  cc3  7598  recexnq  7721  ltbtwnnqq  7746  addnnnq0  7780  mulnnnq0  7781  prarloclemn  7830  prarloc  7834  distrlem1prl  7913  distrlem1pru  7914  distrlem4prl  7915  distrlem4pru  7916  ltexprlemrl  7941  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  addsrpr  8076  mulsrpr  8077  map2psrprg  8136  axpre-suploclemres  8232  lemul12a  9156  lemulge11  9160  sup3exmid  9251  nngt0  9282  nn0ge0  9541  nn0ge2m1nn  9580  zletric  9641  zlelttric  9642  nn0n0n1ge2b  9678  nn0ind-raph  9716  supinfneg  9948  infsupneg  9949  infregelbex  9951  rpge0  10020  fz0fzelfz0  10486  fz0fzdiffz0  10489  ige2m2fzo  10568  elfzodifsumelfzo  10571  elfzom1elp1fzo  10572  exfzdc  10611  zsupcllemstep  10614  infssuzex  10618  qletric  10628  qlelttric  10629  rebtwn2zlemshrink  10640  frecuzrdgtcl  10801  frecuzrdg0  10802  frecuzrdgfunlem  10808  frecuzrdg0t  10811  frecuzrdgsuctlem  10812  frecfzennn  10815  seq3f1olemstep  10903  expcl2lemap  10940  leexp1a  10983  expnbnd  11053  faclbnd  11131  faclbnd6  11134  facavg  11136  fihasheqf1oi  11178  fihashf1rn  11179  fihashss  11209  fiubm  11223  seq3coll  11242  wrdsymb0  11285  wrdlenge2n0  11288  ccatsymb  11318  pfxnd  11409  pfxccat1  11422  swrdpfx  11427  pfxpfx  11428  wrd2ind  11443  pfxccatin12  11453  pfxccat3  11454  swrdccat  11455  pfxccatpfx1  11456  pfxccatpfx2  11457  swrdccatin1d  11463  pfxccatin12d  11465  resqrexlemdecn  11726  qabsor  11789  cau3lem  11828  xrmaxiflemab  11961  xrmaxadd  11975  climcn2  12023  sumeq2  12073  sumrbdclem  12092  summodclem3  12095  summodclem2a  12096  zsumdc  12099  fsumgcl  12101  fsum3  12102  isumss  12106  fsumadd  12121  fsum2dlemstep  12149  fisum0diag2  12162  fsummulc2  12163  modfsummodlemstep  12172  fsumabs  12180  fsumrelem  12186  fsumiun  12192  isumshft  12205  mertenslem2  12251  prodeq2  12272  prodrbdclem  12286  prodmodclem3  12290  prodmodclem2a  12291  zproddc  12294  fprodseq  12298  fprodmul  12306  fprodconst  12335  fprodap0  12336  fprod2dlemstep  12337  fprodrec  12344  fprodsplit1f  12349  fprodap0f  12351  fprodle  12355  sin02gt0  12479  efieq1re  12487  p1modz1  12509  dvdsleabs2  12561  4dvdseven  12632  bitsfzo  12670  bitsinv1lem  12676  gcdeq0  12702  rppwr  12753  uzwodc  12762  algfx  12778  eucalgcvga  12784  lcmmndc  12788  lcmeq0  12797  qredeq  12822  isprm3  12844  rpexp  12879  sqpweven  12901  2sqpwodd  12902  phicl2  12940  phibnd  12943  phiprmpw  12948  fermltl  12960  pythagtriplem4  12995  pythagtriplem6  12997  pythagtriplem7  12998  pythagtriplem12  13002  pythagtriplem13  13003  pythagtriplem14  13004  pythagtriplem16  13006  pcdvdsb  13047  pc2dvds  13057  difsqpwdvds  13065  pcmpt  13070  pcmptdvds  13072  fldivp1  13075  prmpwdvds  13082  infpnlem1  13086  1arith  13094  4sqlem11  13128  ballotfilemfp1  13179  ballotfilemic  13198  ennnfonelemk  13239  ennnfonelemhom  13254  ennnfonelemrnh  13255  ennnfonelemf1  13257  ctinf  13269  ctiunctlemudc  13276  ctiunctlemf  13277  nninfdclemp1  13289  strslfvd  13342  strslfv2d  13343  strslssd  13347  imasival  13574  imasbas  13575  imasplusg  13576  imasaddfnlemg  13582  imasaddvallemg  13583  qusaddvallemg  13601  qusaddflemg  13602  qusaddval  13603  qusaddf  13604  qusmulval  13605  qusmulf  13606  lidrididd  13649  gsumfzval  13658  sgrpidmndm  13685  gsumfzz  13754  qusgrp2  13870  mulgnegnn  13889  eqgen  13984  rinvmod  14066  gsumfzconst  14098  gfsump1  14112  qusrng  14201  srgdilem  14216  ringdilem  14259  qusring2  14313  lssintclm  14662  gsumfzfsumlemm  14865  mplsubgfilemm  14983  eltg3  15052  iuncld  15110  cnss2  15222  txcnp  15266  uptx  15269  xblm  15412  metss  15489  fsumcncntop  15562  rescncf  15576  dedekindeulemlu  15616  suplociccex  15620  dedekindicclemlu  15625  dedekindicc  15628  ivthdec  15639  limccnp2lem  15671  dvaddxx  15698  dvmulxx  15699  dvrecap  15708  reeff1olem  15766  perfectlem2  15998  lgsval  16007  lgsfvalg  16008  lgsfcl2  16009  lgscllem  16010  lgsval2lem  16013  lgsneg  16027  lgsdir2  16036  lgsdir  16038  lgsdi  16040  lgsne0  16041  lgsdirnn0  16050  lgsdinn0  16051  gausslemma2dlem0c  16054  m1lgs  16088  2lgslem1  16094  2lgs  16107  2lgsoddprm  16116  2sqlem6  16123  incistruhgr  16215  upgredg  16269  uhgr2edg  16331  usgriedgdomord  16350  wlkpropg  16449  wlkvtxeledgg  16469  wlk2f  16476  clwwlknonccat  16558  clwwlknonex2lem2  16563  eupth2lem3lem4fi  16598  eupth2lem3lem7fi  16599  dichmul0orlem3  16639  sumdc2  16711  pwle2  16912  subctctexmid  16914  nninfsellemeq  16932  nnnninfex  16940  exmidsbthrlem  16942  cndcap  16984