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  652  jcnd  654  annimdc  940  pm4.55dc  941  orandc  942  dn1dc  963  syl2an23an  1312  xordidc  1419  nfimd  1609  exlimd2  1619  elex22  2792  elex2  2793  spcimdv  2864  spcimedv  2866  spcedv  2869  rspcdva  2889  elabd  2925  spsbcd  3018  opth  4299  euotd  4317  ssorduni  4553  tfisi  4653  omsinds  4688  nnpredcl  4689  sotri2  5099  sotri3  5100  unielrel  5229  funmo  5305  fnfvima  5842  fliftfun  5888  fliftval  5892  riota5f  5947  riotass2  5949  fovcld  6073  oprssdmm  6280  tfrlem5  6423  tfrlemibxssdm  6436  tfrlemibfn  6437  tfrlemiex  6440  tfr1onlemsucfn  6449  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfr1onlemex  6456  tfr1onlemres  6458  tfrcllemsucfn  6462  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllembfn  6466  tfrcllemex  6469  tfrcllemres  6471  tfrcl  6473  rdgisucinc  6494  frecabex  6507  frecabcl  6508  nntr2  6612  ertr  6658  qliftlem  6723  th3q  6750  resixp  6843  f1dom2g  6870  dom3d  6888  domssr  6892  en1  6914  xpdom3m  6954  xpf1o  6966  phplem4dom  6984  phpm  6988  phpelm  6989  findcard  7011  finexdc  7025  fiintim  7054  fisseneq  7057  ssfirab  7059  opabfi  7061  f1dmvrnfibi  7072  iunfidisj  7074  fidcenumlemrk  7082  dcfi  7109  suplub2ti  7129  supelti  7130  ordiso2  7163  caseinl  7219  caseinr  7220  djudom  7221  difinfsn  7228  difinfinf  7229  ctm  7237  enumct  7243  nnnninfeq  7256  ismkvnex  7283  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  acfun  7350  exmidontriimlem2  7365  exmidontriimlem3  7366  exmidapne  7407  cc2lem  7413  cc3  7415  recexnq  7538  ltbtwnnqq  7563  addnnnq0  7597  mulnnnq0  7598  prarloclemn  7647  prarloc  7651  distrlem1prl  7730  distrlem1pru  7731  distrlem4prl  7732  distrlem4pru  7733  ltexprlemrl  7758  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  addsrpr  7893  mulsrpr  7894  map2psrprg  7953  axpre-suploclemres  8049  lemul12a  8970  lemulge11  8974  sup3exmid  9065  nngt0  9096  nn0ge0  9355  nn0ge2m1nn  9390  zletric  9451  zlelttric  9452  nn0n0n1ge2b  9487  nn0ind-raph  9525  supinfneg  9751  infsupneg  9752  infregelbex  9754  rpge0  9823  fz0fzelfz0  10284  fz0fzdiffz0  10287  ige2m2fzo  10364  elfzodifsumelfzo  10367  elfzom1elp1fzo  10368  exfzdc  10406  zsupcllemstep  10409  infssuzex  10413  qletric  10421  qlelttric  10422  rebtwn2zlemshrink  10433  frecuzrdgtcl  10594  frecuzrdg0  10595  frecuzrdgfunlem  10601  frecuzrdg0t  10604  frecuzrdgsuctlem  10605  frecfzennn  10608  seq3f1olemstep  10696  expcl2lemap  10733  leexp1a  10776  expnbnd  10845  faclbnd  10923  faclbnd6  10926  facavg  10928  fihasheqf1oi  10969  fihashf1rn  10970  fihashss  10998  fiubm  11010  seq3coll  11024  wrdsymb0  11063  wrdlenge2n0  11066  ccatsymb  11096  pfxnd  11180  pfxccat1  11193  swrdpfx  11198  pfxpfx  11199  wrd2ind  11214  pfxccatin12  11224  pfxccat3  11225  swrdccat  11226  pfxccatpfx1  11227  pfxccatpfx2  11228  swrdccatin1d  11234  pfxccatin12d  11236  resqrexlemdecn  11438  qabsor  11501  cau3lem  11540  xrmaxiflemab  11673  xrmaxadd  11687  climcn2  11735  sumeq2  11785  sumrbdclem  11803  summodclem3  11806  summodclem2a  11807  zsumdc  11810  fsumgcl  11812  fsum3  11813  isumss  11817  fsumadd  11832  fsum2dlemstep  11860  fisum0diag2  11873  fsummulc2  11874  modfsummodlemstep  11883  fsumabs  11891  fsumrelem  11897  fsumiun  11903  isumshft  11916  mertenslem2  11962  prodeq2  11983  prodrbdclem  11997  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  fprodmul  12017  fprodconst  12046  fprodap0  12047  fprod2dlemstep  12048  fprodrec  12055  fprodsplit1f  12060  fprodap0f  12062  fprodle  12066  sin02gt0  12190  efieq1re  12198  p1modz1  12220  dvdsleabs2  12272  4dvdseven  12343  bitsfzo  12381  bitsinv1lem  12387  gcdeq0  12413  rppwr  12464  uzwodc  12473  algfx  12489  eucalgcvga  12495  lcmmndc  12499  lcmeq0  12508  qredeq  12533  isprm3  12555  rpexp  12590  sqpweven  12612  2sqpwodd  12613  phicl2  12651  phibnd  12654  phiprmpw  12659  fermltl  12671  pythagtriplem4  12706  pythagtriplem6  12708  pythagtriplem7  12709  pythagtriplem12  12713  pythagtriplem13  12714  pythagtriplem14  12715  pythagtriplem16  12717  pcdvdsb  12758  pc2dvds  12768  difsqpwdvds  12776  pcmpt  12781  pcmptdvds  12783  fldivp1  12786  prmpwdvds  12793  infpnlem1  12797  1arith  12805  4sqlem11  12839  ennnfonelemk  12886  ennnfonelemhom  12901  ennnfonelemrnh  12902  ennnfonelemf1  12904  ctinf  12916  ctiunctlemudc  12923  ctiunctlemf  12924  nninfdclemp1  12936  strslfvd  12989  strslfv2d  12990  strslssd  12994  imasival  13253  imasbas  13254  imasplusg  13255  imasaddfnlemg  13261  imasaddvallemg  13262  qusaddvallemg  13280  qusaddflemg  13281  qusaddval  13282  qusaddf  13283  qusmulval  13284  qusmulf  13285  lidrididd  13329  gsumfzval  13338  sgrpidmndm  13367  gsumfzz  13442  qusgrp2  13564  mulgnegnn  13583  eqgen  13678  rinvmod  13760  gsumfzconst  13792  qusrng  13835  srgdilem  13846  ringdilem  13889  qusring2  13943  lssintclm  14261  gsumfzfsumlemm  14464  mplsubgfilemm  14575  eltg3  14644  iuncld  14702  cnss2  14814  txcnp  14858  uptx  14861  xblm  15004  metss  15081  fsumcncntop  15154  rescncf  15168  dedekindeulemlu  15208  suplociccex  15212  dedekindicclemlu  15217  dedekindicc  15220  ivthdec  15231  limccnp2lem  15263  dvaddxx  15290  dvmulxx  15291  dvrecap  15300  reeff1olem  15358  perfectlem2  15587  lgsval  15596  lgsfvalg  15597  lgsfcl2  15598  lgscllem  15599  lgsval2lem  15602  lgsneg  15616  lgsdir2  15625  lgsdir  15627  lgsdi  15629  lgsne0  15630  lgsdirnn0  15639  lgsdinn0  15640  gausslemma2dlem0c  15643  m1lgs  15677  2lgslem1  15683  2lgs  15696  2lgsoddprm  15705  2sqlem6  15712  incistruhgr  15801  upgredg  15848  sumdc2  15935  pwle2  16137  subctctexmid  16139  nninfsellemeq  16153  nnnninfex  16161  exmidsbthrlem  16163  cndcap  16200