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  654  jcnd  656  annimdc  943  pm4.55dc  944  orandc  945  dn1dc  966  syl2an23an  1333  xordidc  1441  nfimd  1631  exlimd2  1641  elex22  2815  elex2  2816  spcimdv  2887  spcimedv  2889  spcedv  2892  rspcdva  2912  elabd  2948  spsbcd  3041  opth  4323  euotd  4341  ssorduni  4579  tfisi  4679  omsinds  4714  nnpredcl  4715  sotri2  5126  sotri3  5127  unielrel  5256  funmo  5333  fnfvima  5878  resfvresima  5880  fliftfun  5926  fliftval  5930  riota5f  5987  riotass2  5989  fovcld  6115  oprssdmm  6323  tfrlem5  6466  tfrlemibxssdm  6479  tfrlemibfn  6480  tfrlemiex  6483  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemex  6499  tfr1onlemres  6501  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemex  6512  tfrcllemres  6514  tfrcl  6516  rdgisucinc  6537  frecabex  6550  frecabcl  6551  nntr2  6657  ertr  6703  qliftlem  6768  th3q  6795  resixp  6888  f1dom2g  6915  dom3d  6933  domssr  6937  en1  6959  xpdom3m  7001  xpf1o  7013  phplem4dom  7031  phpm  7035  phpelm  7036  findcard  7058  finexdc  7073  fiintim  7104  fisseneq  7107  ssfirab  7109  opabfi  7111  f1dmvrnfibi  7122  iunfidisj  7124  fidcenumlemrk  7132  dcfi  7159  suplub2ti  7179  supelti  7180  ordiso2  7213  caseinl  7269  caseinr  7270  djudom  7271  difinfsn  7278  difinfinf  7279  ctm  7287  enumct  7293  nnnninfeq  7306  ismkvnex  7333  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  acfun  7400  exmidontriimlem2  7415  exmidontriimlem3  7416  exmidapne  7457  cc2lem  7463  cc3  7465  recexnq  7588  ltbtwnnqq  7613  addnnnq0  7647  mulnnnq0  7648  prarloclemn  7697  prarloc  7701  distrlem1prl  7780  distrlem1pru  7781  distrlem4prl  7782  distrlem4pru  7783  ltexprlemrl  7808  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  addsrpr  7943  mulsrpr  7944  map2psrprg  8003  axpre-suploclemres  8099  lemul12a  9020  lemulge11  9024  sup3exmid  9115  nngt0  9146  nn0ge0  9405  nn0ge2m1nn  9440  zletric  9501  zlelttric  9502  nn0n0n1ge2b  9537  nn0ind-raph  9575  supinfneg  9802  infsupneg  9803  infregelbex  9805  rpge0  9874  fz0fzelfz0  10335  fz0fzdiffz0  10338  ige2m2fzo  10416  elfzodifsumelfzo  10419  elfzom1elp1fzo  10420  exfzdc  10458  zsupcllemstep  10461  infssuzex  10465  qletric  10473  qlelttric  10474  rebtwn2zlemshrink  10485  frecuzrdgtcl  10646  frecuzrdg0  10647  frecuzrdgfunlem  10653  frecuzrdg0t  10656  frecuzrdgsuctlem  10657  frecfzennn  10660  seq3f1olemstep  10748  expcl2lemap  10785  leexp1a  10828  expnbnd  10897  faclbnd  10975  faclbnd6  10978  facavg  10980  fihasheqf1oi  11021  fihashf1rn  11022  fihashss  11051  fiubm  11063  seq3coll  11077  wrdsymb0  11117  wrdlenge2n0  11120  ccatsymb  11150  pfxnd  11236  pfxccat1  11249  swrdpfx  11254  pfxpfx  11255  wrd2ind  11270  pfxccatin12  11280  pfxccat3  11281  swrdccat  11282  pfxccatpfx1  11283  pfxccatpfx2  11284  swrdccatin1d  11290  pfxccatin12d  11292  resqrexlemdecn  11538  qabsor  11601  cau3lem  11640  xrmaxiflemab  11773  xrmaxadd  11787  climcn2  11835  sumeq2  11885  sumrbdclem  11903  summodclem3  11906  summodclem2a  11907  zsumdc  11910  fsumgcl  11912  fsum3  11913  isumss  11917  fsumadd  11932  fsum2dlemstep  11960  fisum0diag2  11973  fsummulc2  11974  modfsummodlemstep  11983  fsumabs  11991  fsumrelem  11997  fsumiun  12003  isumshft  12016  mertenslem2  12062  prodeq2  12083  prodrbdclem  12097  prodmodclem3  12101  prodmodclem2a  12102  zproddc  12105  fprodseq  12109  fprodmul  12117  fprodconst  12146  fprodap0  12147  fprod2dlemstep  12148  fprodrec  12155  fprodsplit1f  12160  fprodap0f  12162  fprodle  12166  sin02gt0  12290  efieq1re  12298  p1modz1  12320  dvdsleabs2  12372  4dvdseven  12443  bitsfzo  12481  bitsinv1lem  12487  gcdeq0  12513  rppwr  12564  uzwodc  12573  algfx  12589  eucalgcvga  12595  lcmmndc  12599  lcmeq0  12608  qredeq  12633  isprm3  12655  rpexp  12690  sqpweven  12712  2sqpwodd  12713  phicl2  12751  phibnd  12754  phiprmpw  12759  fermltl  12771  pythagtriplem4  12806  pythagtriplem6  12808  pythagtriplem7  12809  pythagtriplem12  12813  pythagtriplem13  12814  pythagtriplem14  12815  pythagtriplem16  12817  pcdvdsb  12858  pc2dvds  12868  difsqpwdvds  12876  pcmpt  12881  pcmptdvds  12883  fldivp1  12886  prmpwdvds  12893  infpnlem1  12897  1arith  12905  4sqlem11  12939  ennnfonelemk  12986  ennnfonelemhom  13001  ennnfonelemrnh  13002  ennnfonelemf1  13004  ctinf  13016  ctiunctlemudc  13023  ctiunctlemf  13024  nninfdclemp1  13036  strslfvd  13089  strslfv2d  13090  strslssd  13094  imasival  13354  imasbas  13355  imasplusg  13356  imasaddfnlemg  13362  imasaddvallemg  13363  qusaddvallemg  13381  qusaddflemg  13382  qusaddval  13383  qusaddf  13384  qusmulval  13385  qusmulf  13386  lidrididd  13430  gsumfzval  13439  sgrpidmndm  13468  gsumfzz  13543  qusgrp2  13665  mulgnegnn  13684  eqgen  13779  rinvmod  13861  gsumfzconst  13893  qusrng  13936  srgdilem  13947  ringdilem  13990  qusring2  14044  lssintclm  14363  gsumfzfsumlemm  14566  mplsubgfilemm  14677  eltg3  14746  iuncld  14804  cnss2  14916  txcnp  14960  uptx  14963  xblm  15106  metss  15183  fsumcncntop  15256  rescncf  15270  dedekindeulemlu  15310  suplociccex  15314  dedekindicclemlu  15319  dedekindicc  15322  ivthdec  15333  limccnp2lem  15365  dvaddxx  15392  dvmulxx  15393  dvrecap  15402  reeff1olem  15460  perfectlem2  15689  lgsval  15698  lgsfvalg  15699  lgsfcl2  15700  lgscllem  15701  lgsval2lem  15704  lgsneg  15718  lgsdir2  15727  lgsdir  15729  lgsdi  15731  lgsne0  15732  lgsdirnn0  15741  lgsdinn0  15742  gausslemma2dlem0c  15745  m1lgs  15779  2lgslem1  15785  2lgs  15798  2lgsoddprm  15807  2sqlem6  15814  incistruhgr  15905  upgredg  15957  uhgr2edg  16019  usgriedgdomord  16038  wlkpropg  16065  wlkvtxeledgg  16085  wlk2f  16092  sumdc2  16218  pwle2  16423  subctctexmid  16425  nninfsellemeq  16440  nnnninfex  16448  exmidsbthrlem  16450  cndcap  16487