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  2819  elex2  2820  spcimdv  2891  spcimedv  2893  spcedv  2896  rspcdva  2916  elabd  2952  spsbcd  3045  opth  4335  euotd  4353  ssorduni  4591  tfisi  4691  omsinds  4726  nnpredcl  4727  sotri2  5141  sotri3  5142  unielrel  5271  funmo  5348  fnfvima  5899  resfvresima  5901  fliftfun  5947  fliftval  5951  riota5f  6008  riotass2  6010  fovcld  6136  oprssdmm  6343  funsssuppss  6436  tfrlem5  6523  tfrlemibxssdm  6536  tfrlemibfn  6537  tfrlemiex  6540  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemex  6556  tfr1onlemres  6558  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemex  6569  tfrcllemres  6571  tfrcl  6573  rdgisucinc  6594  frecabex  6607  frecabcl  6608  nntr2  6714  ertr  6760  qliftlem  6825  th3q  6852  resixp  6945  f1dom2g  6972  dom3d  6990  domssr  6994  en1  7016  xpdom3m  7061  xpf1o  7073  phplem4dom  7091  phpm  7095  phpelm  7096  findcard  7120  finexdc  7135  fiintim  7166  fisseneq  7170  ssfirab  7172  opabfi  7175  f1dmvrnfibi  7186  iunfidisj  7188  fidcenumlemrk  7196  dcfi  7223  suplub2ti  7243  supelti  7244  ordiso2  7277  caseinl  7333  caseinr  7334  djudom  7335  difinfsn  7342  difinfinf  7343  ctm  7351  enumct  7357  nnnninfeq  7370  ismkvnex  7397  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  acfun  7465  exmidontriimlem2  7480  exmidontriimlem3  7481  exmidapne  7522  cc2lem  7528  cc3  7530  recexnq  7653  ltbtwnnqq  7678  addnnnq0  7712  mulnnnq0  7713  prarloclemn  7762  prarloc  7766  distrlem1prl  7845  distrlem1pru  7846  distrlem4prl  7847  distrlem4pru  7848  ltexprlemrl  7873  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  addsrpr  8008  mulsrpr  8009  map2psrprg  8068  axpre-suploclemres  8164  lemul12a  9084  lemulge11  9088  sup3exmid  9179  nngt0  9210  nn0ge0  9469  nn0ge2m1nn  9506  zletric  9567  zlelttric  9568  nn0n0n1ge2b  9603  nn0ind-raph  9641  supinfneg  9873  infsupneg  9874  infregelbex  9876  rpge0  9945  fz0fzelfz0  10407  fz0fzdiffz0  10410  ige2m2fzo  10489  elfzodifsumelfzo  10492  elfzom1elp1fzo  10493  exfzdc  10532  zsupcllemstep  10535  infssuzex  10539  qletric  10547  qlelttric  10548  rebtwn2zlemshrink  10559  frecuzrdgtcl  10720  frecuzrdg0  10721  frecuzrdgfunlem  10727  frecuzrdg0t  10730  frecuzrdgsuctlem  10731  frecfzennn  10734  seq3f1olemstep  10822  expcl2lemap  10859  leexp1a  10902  expnbnd  10971  faclbnd  11049  faclbnd6  11052  facavg  11054  fihasheqf1oi  11095  fihashf1rn  11096  fihashss  11126  fiubm  11138  seq3coll  11152  wrdsymb0  11195  wrdlenge2n0  11198  ccatsymb  11228  pfxnd  11319  pfxccat1  11332  swrdpfx  11337  pfxpfx  11338  wrd2ind  11353  pfxccatin12  11363  pfxccat3  11364  swrdccat  11365  pfxccatpfx1  11366  pfxccatpfx2  11367  swrdccatin1d  11373  pfxccatin12d  11375  resqrexlemdecn  11635  qabsor  11698  cau3lem  11737  xrmaxiflemab  11870  xrmaxadd  11884  climcn2  11932  sumeq2  11982  sumrbdclem  12001  summodclem3  12004  summodclem2a  12005  zsumdc  12008  fsumgcl  12010  fsum3  12011  isumss  12015  fsumadd  12030  fsum2dlemstep  12058  fisum0diag2  12071  fsummulc2  12072  modfsummodlemstep  12081  fsumabs  12089  fsumrelem  12095  fsumiun  12101  isumshft  12114  mertenslem2  12160  prodeq2  12181  prodrbdclem  12195  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  fprodmul  12215  fprodconst  12244  fprodap0  12245  fprod2dlemstep  12246  fprodrec  12253  fprodsplit1f  12258  fprodap0f  12260  fprodle  12264  sin02gt0  12388  efieq1re  12396  p1modz1  12418  dvdsleabs2  12470  4dvdseven  12541  bitsfzo  12579  bitsinv1lem  12585  gcdeq0  12611  rppwr  12662  uzwodc  12671  algfx  12687  eucalgcvga  12693  lcmmndc  12697  lcmeq0  12706  qredeq  12731  isprm3  12753  rpexp  12788  sqpweven  12810  2sqpwodd  12811  phicl2  12849  phibnd  12852  phiprmpw  12857  fermltl  12869  pythagtriplem4  12904  pythagtriplem6  12906  pythagtriplem7  12907  pythagtriplem12  12911  pythagtriplem13  12912  pythagtriplem14  12913  pythagtriplem16  12915  pcdvdsb  12956  pc2dvds  12966  difsqpwdvds  12974  pcmpt  12979  pcmptdvds  12981  fldivp1  12984  prmpwdvds  12991  infpnlem1  12995  1arith  13003  4sqlem11  13037  ennnfonelemk  13084  ennnfonelemhom  13099  ennnfonelemrnh  13100  ennnfonelemf1  13102  ctinf  13114  ctiunctlemudc  13121  ctiunctlemf  13122  nninfdclemp1  13134  strslfvd  13187  strslfv2d  13188  strslssd  13192  imasival  13452  imasbas  13453  imasplusg  13454  imasaddfnlemg  13460  imasaddvallemg  13461  qusaddvallemg  13479  qusaddflemg  13480  qusaddval  13481  qusaddf  13482  qusmulval  13483  qusmulf  13484  lidrididd  13528  gsumfzval  13537  sgrpidmndm  13566  gsumfzz  13641  qusgrp2  13763  mulgnegnn  13782  eqgen  13877  rinvmod  13959  gsumfzconst  13991  qusrng  14035  srgdilem  14046  ringdilem  14089  qusring2  14143  lssintclm  14463  gsumfzfsumlemm  14666  mplsubgfilemm  14782  eltg3  14851  iuncld  14909  cnss2  15021  txcnp  15065  uptx  15068  xblm  15211  metss  15288  fsumcncntop  15361  rescncf  15375  dedekindeulemlu  15415  suplociccex  15419  dedekindicclemlu  15424  dedekindicc  15427  ivthdec  15438  limccnp2lem  15470  dvaddxx  15497  dvmulxx  15498  dvrecap  15507  reeff1olem  15565  perfectlem2  15797  lgsval  15806  lgsfvalg  15807  lgsfcl2  15808  lgscllem  15809  lgsval2lem  15812  lgsneg  15826  lgsdir2  15835  lgsdir  15837  lgsdi  15839  lgsne0  15840  lgsdirnn0  15849  lgsdinn0  15850  gausslemma2dlem0c  15853  m1lgs  15887  2lgslem1  15893  2lgs  15906  2lgsoddprm  15915  2sqlem6  15922  incistruhgr  16014  upgredg  16068  uhgr2edg  16130  usgriedgdomord  16149  wlkpropg  16248  wlkvtxeledgg  16268  wlk2f  16275  clwwlknonccat  16357  clwwlknonex2lem2  16362  eupth2lem3lem4fi  16397  eupth2lem3lem7fi  16398  sumdc2  16500  pwle2  16703  subctctexmid  16705  nninfsellemeq  16723  nnnninfex  16731  exmidsbthrlem  16733  cndcap  16775  gfsump1  16798