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  651  jcnd  653  annimdc  939  pm4.55dc  940  orandc  941  dn1dc  962  syl2an23an  1310  xordidc  1410  nfimd  1599  exlimd2  1609  elex22  2778  elex2  2779  spcimdv  2848  spcimedv  2850  spcedv  2853  rspcdva  2873  elabd  2909  spsbcd  3002  opth  4271  euotd  4288  ssorduni  4524  tfisi  4624  omsinds  4659  nnpredcl  4660  sotri2  5068  sotri3  5069  unielrel  5198  funmo  5274  fnfvima  5800  fliftfun  5846  fliftval  5850  riota5f  5905  riotass2  5907  fovcld  6031  oprssdmm  6238  tfrlem5  6381  tfrlemibxssdm  6394  tfrlemibfn  6395  tfrlemiex  6398  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemex  6414  tfr1onlemres  6416  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemex  6427  tfrcllemres  6429  tfrcl  6431  rdgisucinc  6452  frecabex  6465  frecabcl  6466  nntr2  6570  ertr  6616  qliftlem  6681  th3q  6708  resixp  6801  f1dom2g  6824  dom3d  6842  en1  6867  xpdom3m  6902  xpf1o  6914  phplem4dom  6932  phpm  6935  phpelm  6936  findcard  6958  finexdc  6972  fiintim  7001  fisseneq  7004  ssfirab  7006  opabfi  7008  f1dmvrnfibi  7019  iunfidisj  7021  fidcenumlemrk  7029  dcfi  7056  suplub2ti  7076  supelti  7077  ordiso2  7110  caseinl  7166  caseinr  7167  djudom  7168  difinfsn  7175  difinfinf  7176  ctm  7184  enumct  7190  nnnninfeq  7203  ismkvnex  7230  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  acfun  7292  exmidontriimlem2  7307  exmidontriimlem3  7308  exmidapne  7345  cc2lem  7351  cc3  7353  recexnq  7476  ltbtwnnqq  7501  addnnnq0  7535  mulnnnq0  7536  prarloclemn  7585  prarloc  7589  distrlem1prl  7668  distrlem1pru  7669  distrlem4prl  7670  distrlem4pru  7671  ltexprlemrl  7696  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  addsrpr  7831  mulsrpr  7832  map2psrprg  7891  axpre-suploclemres  7987  lemul12a  8908  lemulge11  8912  sup3exmid  9003  nngt0  9034  nn0ge0  9293  nn0ge2m1nn  9328  zletric  9389  zlelttric  9390  nn0n0n1ge2b  9424  nn0ind-raph  9462  supinfneg  9688  infsupneg  9689  infregelbex  9691  rpge0  9760  fz0fzelfz0  10221  fz0fzdiffz0  10224  ige2m2fzo  10293  elfzodifsumelfzo  10296  elfzom1elp1fzo  10297  exfzdc  10335  zsupcllemstep  10338  infssuzex  10342  qletric  10350  qlelttric  10351  rebtwn2zlemshrink  10362  frecuzrdgtcl  10523  frecuzrdg0  10524  frecuzrdgfunlem  10530  frecuzrdg0t  10533  frecuzrdgsuctlem  10534  frecfzennn  10537  seq3f1olemstep  10625  expcl2lemap  10662  leexp1a  10705  expnbnd  10774  faclbnd  10852  faclbnd6  10855  facavg  10857  fihasheqf1oi  10898  fihashf1rn  10899  fihashss  10927  fiubm  10939  seq3coll  10953  wrdsymb0  10986  wrdlenge2n0  10989  resqrexlemdecn  11196  qabsor  11259  cau3lem  11298  xrmaxiflemab  11431  xrmaxadd  11445  climcn2  11493  sumeq2  11543  sumrbdclem  11561  summodclem3  11564  summodclem2a  11565  zsumdc  11568  fsumgcl  11570  fsum3  11571  isumss  11575  fsumadd  11590  fsum2dlemstep  11618  fisum0diag2  11631  fsummulc2  11632  modfsummodlemstep  11641  fsumabs  11649  fsumrelem  11655  fsumiun  11661  isumshft  11674  mertenslem2  11720  prodeq2  11741  prodrbdclem  11755  prodmodclem3  11759  prodmodclem2a  11760  zproddc  11763  fprodseq  11767  fprodmul  11775  fprodconst  11804  fprodap0  11805  fprod2dlemstep  11806  fprodrec  11813  fprodsplit1f  11818  fprodap0f  11820  fprodle  11824  sin02gt0  11948  efieq1re  11956  p1modz1  11978  dvdsleabs2  12030  4dvdseven  12101  bitsfzo  12139  bitsinv1lem  12145  gcdeq0  12171  rppwr  12222  uzwodc  12231  algfx  12247  eucalgcvga  12253  lcmmndc  12257  lcmeq0  12266  qredeq  12291  isprm3  12313  rpexp  12348  sqpweven  12370  2sqpwodd  12371  phicl2  12409  phibnd  12412  phiprmpw  12417  fermltl  12429  pythagtriplem4  12464  pythagtriplem6  12466  pythagtriplem7  12467  pythagtriplem12  12471  pythagtriplem13  12472  pythagtriplem14  12473  pythagtriplem16  12475  pcdvdsb  12516  pc2dvds  12526  difsqpwdvds  12534  pcmpt  12539  pcmptdvds  12541  fldivp1  12544  prmpwdvds  12551  infpnlem1  12555  1arith  12563  4sqlem11  12597  ennnfonelemk  12644  ennnfonelemhom  12659  ennnfonelemrnh  12660  ennnfonelemf1  12662  ctinf  12674  ctiunctlemudc  12681  ctiunctlemf  12682  nninfdclemp1  12694  strslfvd  12747  strslfv2d  12748  strslssd  12752  imasival  13010  imasbas  13011  imasplusg  13012  imasaddfnlemg  13018  imasaddvallemg  13019  qusaddvallemg  13037  qusaddflemg  13038  qusaddval  13039  qusaddf  13040  qusmulval  13041  qusmulf  13042  lidrididd  13086  gsumfzval  13095  sgrpidmndm  13124  gsumfzz  13199  qusgrp2  13321  mulgnegnn  13340  eqgen  13435  rinvmod  13517  gsumfzconst  13549  qusrng  13592  srgdilem  13603  ringdilem  13646  qusring2  13700  lssintclm  14018  gsumfzfsumlemm  14221  mplsubgfilemm  14332  eltg3  14401  iuncld  14459  cnss2  14571  txcnp  14615  uptx  14618  xblm  14761  metss  14838  fsumcncntop  14911  rescncf  14925  dedekindeulemlu  14965  suplociccex  14969  dedekindicclemlu  14974  dedekindicc  14977  ivthdec  14988  limccnp2lem  15020  dvaddxx  15047  dvmulxx  15048  dvrecap  15057  reeff1olem  15115  perfectlem2  15344  lgsval  15353  lgsfvalg  15354  lgsfcl2  15355  lgscllem  15356  lgsval2lem  15359  lgsneg  15373  lgsdir2  15382  lgsdir  15384  lgsdi  15386  lgsne0  15387  lgsdirnn0  15396  lgsdinn0  15397  gausslemma2dlem0c  15400  m1lgs  15434  2lgslem1  15440  2lgs  15453  2lgsoddprm  15462  2sqlem6  15469  sumdc2  15553  pwle2  15753  subctctexmid  15755  nninfsellemeq  15769  nnnninfex  15777  exmidsbthrlem  15779  cndcap  15816