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  945  pm4.55dc  946  orandc  947  dn1dc  968  syl2an23an  1335  xordidc  1443  nfimd  1633  exlimd2  1643  elex22  2818  elex2  2819  spcimdv  2890  spcimedv  2892  spcedv  2895  rspcdva  2915  elabd  2951  spsbcd  3044  opth  4329  euotd  4347  ssorduni  4585  tfisi  4685  omsinds  4720  nnpredcl  4721  sotri2  5134  sotri3  5135  unielrel  5264  funmo  5341  fnfvima  5889  resfvresima  5891  fliftfun  5937  fliftval  5941  riota5f  5998  riotass2  6000  fovcld  6126  oprssdmm  6334  tfrlem5  6480  tfrlemibxssdm  6493  tfrlemibfn  6494  tfrlemiex  6497  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemex  6513  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemex  6526  tfrcllemres  6528  tfrcl  6530  rdgisucinc  6551  frecabex  6564  frecabcl  6565  nntr2  6671  ertr  6717  qliftlem  6782  th3q  6809  resixp  6902  f1dom2g  6929  dom3d  6947  domssr  6951  en1  6973  xpdom3m  7018  xpf1o  7030  phplem4dom  7048  phpm  7052  phpelm  7053  findcard  7077  finexdc  7092  fiintim  7123  fisseneq  7127  ssfirab  7129  opabfi  7132  f1dmvrnfibi  7143  iunfidisj  7145  fidcenumlemrk  7153  dcfi  7180  suplub2ti  7200  supelti  7201  ordiso2  7234  caseinl  7290  caseinr  7291  djudom  7292  difinfsn  7299  difinfinf  7300  ctm  7308  enumct  7314  nnnninfeq  7327  ismkvnex  7354  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  acfun  7422  exmidontriimlem2  7437  exmidontriimlem3  7438  exmidapne  7479  cc2lem  7485  cc3  7487  recexnq  7610  ltbtwnnqq  7635  addnnnq0  7669  mulnnnq0  7670  prarloclemn  7719  prarloc  7723  distrlem1prl  7802  distrlem1pru  7803  distrlem4prl  7804  distrlem4pru  7805  ltexprlemrl  7830  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  addsrpr  7965  mulsrpr  7966  map2psrprg  8025  axpre-suploclemres  8121  lemul12a  9042  lemulge11  9046  sup3exmid  9137  nngt0  9168  nn0ge0  9427  nn0ge2m1nn  9462  zletric  9523  zlelttric  9524  nn0n0n1ge2b  9559  nn0ind-raph  9597  supinfneg  9829  infsupneg  9830  infregelbex  9832  rpge0  9901  fz0fzelfz0  10362  fz0fzdiffz0  10365  ige2m2fzo  10444  elfzodifsumelfzo  10447  elfzom1elp1fzo  10448  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  qletric  10502  qlelttric  10503  rebtwn2zlemshrink  10514  frecuzrdgtcl  10675  frecuzrdg0  10676  frecuzrdgfunlem  10682  frecuzrdg0t  10685  frecuzrdgsuctlem  10686  frecfzennn  10689  seq3f1olemstep  10777  expcl2lemap  10814  leexp1a  10857  expnbnd  10926  faclbnd  11004  faclbnd6  11007  facavg  11009  fihasheqf1oi  11050  fihashf1rn  11051  fihashss  11081  fiubm  11093  seq3coll  11107  wrdsymb0  11150  wrdlenge2n0  11153  ccatsymb  11183  pfxnd  11274  pfxccat1  11287  swrdpfx  11292  pfxpfx  11293  wrd2ind  11308  pfxccatin12  11318  pfxccat3  11319  swrdccat  11320  pfxccatpfx1  11321  pfxccatpfx2  11322  swrdccatin1d  11328  pfxccatin12d  11330  resqrexlemdecn  11590  qabsor  11653  cau3lem  11692  xrmaxiflemab  11825  xrmaxadd  11839  climcn2  11887  sumeq2  11937  sumrbdclem  11956  summodclem3  11959  summodclem2a  11960  zsumdc  11963  fsumgcl  11965  fsum3  11966  isumss  11970  fsumadd  11985  fsum2dlemstep  12013  fisum0diag2  12026  fsummulc2  12027  modfsummodlemstep  12036  fsumabs  12044  fsumrelem  12050  fsumiun  12056  isumshft  12069  mertenslem2  12115  prodeq2  12136  prodrbdclem  12150  prodmodclem3  12154  prodmodclem2a  12155  zproddc  12158  fprodseq  12162  fprodmul  12170  fprodconst  12199  fprodap0  12200  fprod2dlemstep  12201  fprodrec  12208  fprodsplit1f  12213  fprodap0f  12215  fprodle  12219  sin02gt0  12343  efieq1re  12351  p1modz1  12373  dvdsleabs2  12425  4dvdseven  12496  bitsfzo  12534  bitsinv1lem  12540  gcdeq0  12566  rppwr  12617  uzwodc  12626  algfx  12642  eucalgcvga  12648  lcmmndc  12652  lcmeq0  12661  qredeq  12686  isprm3  12708  rpexp  12743  sqpweven  12765  2sqpwodd  12766  phicl2  12804  phibnd  12807  phiprmpw  12812  fermltl  12824  pythagtriplem4  12859  pythagtriplem6  12861  pythagtriplem7  12862  pythagtriplem12  12866  pythagtriplem13  12867  pythagtriplem14  12868  pythagtriplem16  12870  pcdvdsb  12911  pc2dvds  12921  difsqpwdvds  12929  pcmpt  12934  pcmptdvds  12936  fldivp1  12939  prmpwdvds  12946  infpnlem1  12950  1arith  12958  4sqlem11  12992  ennnfonelemk  13039  ennnfonelemhom  13054  ennnfonelemrnh  13055  ennnfonelemf1  13057  ctinf  13069  ctiunctlemudc  13076  ctiunctlemf  13077  nninfdclemp1  13089  strslfvd  13142  strslfv2d  13143  strslssd  13147  imasival  13407  imasbas  13408  imasplusg  13409  imasaddfnlemg  13415  imasaddvallemg  13416  qusaddvallemg  13434  qusaddflemg  13435  qusaddval  13436  qusaddf  13437  qusmulval  13438  qusmulf  13439  lidrididd  13483  gsumfzval  13492  sgrpidmndm  13521  gsumfzz  13596  qusgrp2  13718  mulgnegnn  13737  eqgen  13832  rinvmod  13914  gsumfzconst  13946  qusrng  13990  srgdilem  14001  ringdilem  14044  qusring2  14098  lssintclm  14417  gsumfzfsumlemm  14620  mplsubgfilemm  14731  eltg3  14800  iuncld  14858  cnss2  14970  txcnp  15014  uptx  15017  xblm  15160  metss  15237  fsumcncntop  15310  rescncf  15324  dedekindeulemlu  15364  suplociccex  15368  dedekindicclemlu  15373  dedekindicc  15376  ivthdec  15387  limccnp2lem  15419  dvaddxx  15446  dvmulxx  15447  dvrecap  15456  reeff1olem  15514  perfectlem2  15743  lgsval  15752  lgsfvalg  15753  lgsfcl2  15754  lgscllem  15755  lgsval2lem  15758  lgsneg  15772  lgsdir2  15781  lgsdir  15783  lgsdi  15785  lgsne0  15786  lgsdirnn0  15795  lgsdinn0  15796  gausslemma2dlem0c  15799  m1lgs  15833  2lgslem1  15839  2lgs  15852  2lgsoddprm  15861  2sqlem6  15868  incistruhgr  15960  upgredg  16014  uhgr2edg  16076  usgriedgdomord  16095  wlkpropg  16194  wlkvtxeledgg  16214  wlk2f  16221  clwwlknonccat  16303  clwwlknonex2lem2  16308  eupth2lem3lem4fi  16343  eupth2lem3lem7fi  16344  sumdc2  16446  pwle2  16650  subctctexmid  16652  nninfsellemeq  16667  nnnninfex  16675  exmidsbthrlem  16677  cndcap  16715  gfsump1  16738