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  9153  lemulge11  9157  sup3exmid  9248  nngt0  9279  nn0ge0  9538  nn0ge2m1nn  9577  zletric  9638  zlelttric  9639  nn0n0n1ge2b  9675  nn0ind-raph  9713  supinfneg  9945  infsupneg  9946  infregelbex  9948  rpge0  10017  fz0fzelfz0  10483  fz0fzdiffz0  10486  ige2m2fzo  10565  elfzodifsumelfzo  10568  elfzom1elp1fzo  10569  exfzdc  10608  zsupcllemstep  10611  infssuzex  10615  qletric  10625  qlelttric  10626  rebtwn2zlemshrink  10637  frecuzrdgtcl  10798  frecuzrdg0  10799  frecuzrdgfunlem  10805  frecuzrdg0t  10808  frecuzrdgsuctlem  10809  frecfzennn  10812  seq3f1olemstep  10900  expcl2lemap  10937  leexp1a  10980  expnbnd  11050  faclbnd  11128  faclbnd6  11131  facavg  11133  fihasheqf1oi  11175  fihashf1rn  11176  fihashss  11206  fiubm  11220  seq3coll  11239  wrdsymb0  11282  wrdlenge2n0  11285  ccatsymb  11315  pfxnd  11406  pfxccat1  11419  swrdpfx  11424  pfxpfx  11425  wrd2ind  11440  pfxccatin12  11450  pfxccat3  11451  swrdccat  11452  pfxccatpfx1  11453  pfxccatpfx2  11454  swrdccatin1d  11460  pfxccatin12d  11462  resqrexlemdecn  11722  qabsor  11785  cau3lem  11824  xrmaxiflemab  11957  xrmaxadd  11971  climcn2  12019  sumeq2  12069  sumrbdclem  12088  summodclem3  12091  summodclem2a  12092  zsumdc  12095  fsumgcl  12097  fsum3  12098  isumss  12102  fsumadd  12117  fsum2dlemstep  12145  fisum0diag2  12158  fsummulc2  12159  modfsummodlemstep  12168  fsumabs  12176  fsumrelem  12182  fsumiun  12188  isumshft  12201  mertenslem2  12247  prodeq2  12268  prodrbdclem  12282  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  fprodmul  12302  fprodconst  12331  fprodap0  12332  fprod2dlemstep  12333  fprodrec  12340  fprodsplit1f  12345  fprodap0f  12347  fprodle  12351  sin02gt0  12475  efieq1re  12483  p1modz1  12505  dvdsleabs2  12557  4dvdseven  12628  bitsfzo  12666  bitsinv1lem  12672  gcdeq0  12698  rppwr  12749  uzwodc  12758  algfx  12774  eucalgcvga  12780  lcmmndc  12784  lcmeq0  12793  qredeq  12818  isprm3  12840  rpexp  12875  sqpweven  12897  2sqpwodd  12898  phicl2  12936  phibnd  12939  phiprmpw  12944  fermltl  12956  pythagtriplem4  12991  pythagtriplem6  12993  pythagtriplem7  12994  pythagtriplem12  12998  pythagtriplem13  12999  pythagtriplem14  13000  pythagtriplem16  13002  pcdvdsb  13043  pc2dvds  13053  difsqpwdvds  13061  pcmpt  13066  pcmptdvds  13068  fldivp1  13071  prmpwdvds  13078  infpnlem1  13082  1arith  13090  4sqlem11  13124  ballotfilemfp1  13175  ballotfilemic  13194  ennnfonelemk  13235  ennnfonelemhom  13250  ennnfonelemrnh  13251  ennnfonelemf1  13253  ctinf  13265  ctiunctlemudc  13272  ctiunctlemf  13273  nninfdclemp1  13285  strslfvd  13338  strslfv2d  13339  strslssd  13343  imasival  13570  imasbas  13571  imasplusg  13572  imasaddfnlemg  13578  imasaddvallemg  13579  qusaddvallemg  13597  qusaddflemg  13598  qusaddval  13599  qusaddf  13600  qusmulval  13601  qusmulf  13602  lidrididd  13645  gsumfzval  13654  sgrpidmndm  13681  gsumfzz  13750  qusgrp2  13866  mulgnegnn  13885  eqgen  13980  rinvmod  14062  gsumfzconst  14094  gfsump1  14108  qusrng  14197  srgdilem  14212  ringdilem  14255  qusring2  14309  lssintclm  14658  gsumfzfsumlemm  14861  mplsubgfilemm  14979  eltg3  15048  iuncld  15106  cnss2  15218  txcnp  15262  uptx  15265  xblm  15408  metss  15485  fsumcncntop  15558  rescncf  15572  dedekindeulemlu  15612  suplociccex  15616  dedekindicclemlu  15621  dedekindicc  15624  ivthdec  15635  limccnp2lem  15667  dvaddxx  15694  dvmulxx  15695  dvrecap  15704  reeff1olem  15762  perfectlem2  15994  lgsval  16003  lgsfvalg  16004  lgsfcl2  16005  lgscllem  16006  lgsval2lem  16009  lgsneg  16023  lgsdir2  16032  lgsdir  16034  lgsdi  16036  lgsne0  16037  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem0c  16050  m1lgs  16084  2lgslem1  16090  2lgs  16103  2lgsoddprm  16112  2sqlem6  16119  incistruhgr  16211  upgredg  16265  uhgr2edg  16327  usgriedgdomord  16346  wlkpropg  16445  wlkvtxeledgg  16465  wlk2f  16472  clwwlknonccat  16554  clwwlknonex2lem2  16559  eupth2lem3lem4fi  16594  eupth2lem3lem7fi  16595  sumdc2  16697  pwle2  16898  subctctexmid  16900  nninfsellemeq  16918  nnnninfex  16926  exmidsbthrlem  16928  cndcap  16970