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  2793  elex2  2794  spcimdv  2865  spcimedv  2867  spcedv  2870  rspcdva  2890  elabd  2926  spsbcd  3019  opth  4300  euotd  4318  ssorduni  4554  tfisi  4654  omsinds  4689  nnpredcl  4690  sotri2  5100  sotri3  5101  unielrel  5230  funmo  5306  fnfvima  5844  fliftfun  5890  fliftval  5894  riota5f  5949  riotass2  5951  fovcld  6075  oprssdmm  6282  tfrlem5  6425  tfrlemibxssdm  6438  tfrlemibfn  6439  tfrlemiex  6442  tfr1onlemsucfn  6451  tfr1onlemsucaccv  6452  tfr1onlembxssdm  6454  tfr1onlembfn  6455  tfr1onlemex  6458  tfr1onlemres  6460  tfrcllemsucfn  6464  tfrcllemsucaccv  6465  tfrcllembxssdm  6467  tfrcllembfn  6468  tfrcllemex  6471  tfrcllemres  6473  tfrcl  6475  rdgisucinc  6496  frecabex  6509  frecabcl  6510  nntr2  6614  ertr  6660  qliftlem  6725  th3q  6752  resixp  6845  f1dom2g  6872  dom3d  6890  domssr  6894  en1  6916  xpdom3m  6956  xpf1o  6968  phplem4dom  6986  phpm  6990  phpelm  6991  findcard  7013  finexdc  7027  fiintim  7056  fisseneq  7059  ssfirab  7061  opabfi  7063  f1dmvrnfibi  7074  iunfidisj  7076  fidcenumlemrk  7084  dcfi  7111  suplub2ti  7131  supelti  7132  ordiso2  7165  caseinl  7221  caseinr  7222  djudom  7223  difinfsn  7230  difinfinf  7231  ctm  7239  enumct  7245  nnnninfeq  7258  ismkvnex  7285  exmidfodomrlemr  7343  exmidfodomrlemrALT  7344  acfun  7352  exmidontriimlem2  7367  exmidontriimlem3  7368  exmidapne  7409  cc2lem  7415  cc3  7417  recexnq  7540  ltbtwnnqq  7565  addnnnq0  7599  mulnnnq0  7600  prarloclemn  7649  prarloc  7653  distrlem1prl  7732  distrlem1pru  7733  distrlem4prl  7734  distrlem4pru  7735  ltexprlemrl  7760  cauappcvgprlemladdru  7806  cauappcvgprlemladdrl  7807  addsrpr  7895  mulsrpr  7896  map2psrprg  7955  axpre-suploclemres  8051  lemul12a  8972  lemulge11  8976  sup3exmid  9067  nngt0  9098  nn0ge0  9357  nn0ge2m1nn  9392  zletric  9453  zlelttric  9454  nn0n0n1ge2b  9489  nn0ind-raph  9527  supinfneg  9753  infsupneg  9754  infregelbex  9756  rpge0  9825  fz0fzelfz0  10286  fz0fzdiffz0  10289  ige2m2fzo  10366  elfzodifsumelfzo  10369  elfzom1elp1fzo  10370  exfzdc  10408  zsupcllemstep  10411  infssuzex  10415  qletric  10423  qlelttric  10424  rebtwn2zlemshrink  10435  frecuzrdgtcl  10596  frecuzrdg0  10597  frecuzrdgfunlem  10603  frecuzrdg0t  10606  frecuzrdgsuctlem  10607  frecfzennn  10610  seq3f1olemstep  10698  expcl2lemap  10735  leexp1a  10778  expnbnd  10847  faclbnd  10925  faclbnd6  10928  facavg  10930  fihasheqf1oi  10971  fihashf1rn  10972  fihashss  11000  fiubm  11012  seq3coll  11026  wrdsymb0  11065  wrdlenge2n0  11068  ccatsymb  11098  pfxnd  11182  pfxccat1  11195  swrdpfx  11200  pfxpfx  11201  wrd2ind  11216  pfxccatin12  11226  pfxccat3  11227  swrdccat  11228  pfxccatpfx1  11229  pfxccatpfx2  11230  swrdccatin1d  11236  pfxccatin12d  11238  resqrexlemdecn  11484  qabsor  11547  cau3lem  11586  xrmaxiflemab  11719  xrmaxadd  11733  climcn2  11781  sumeq2  11831  sumrbdclem  11849  summodclem3  11852  summodclem2a  11853  zsumdc  11856  fsumgcl  11858  fsum3  11859  isumss  11863  fsumadd  11878  fsum2dlemstep  11906  fisum0diag2  11919  fsummulc2  11920  modfsummodlemstep  11929  fsumabs  11937  fsumrelem  11943  fsumiun  11949  isumshft  11962  mertenslem2  12008  prodeq2  12029  prodrbdclem  12043  prodmodclem3  12047  prodmodclem2a  12048  zproddc  12051  fprodseq  12055  fprodmul  12063  fprodconst  12092  fprodap0  12093  fprod2dlemstep  12094  fprodrec  12101  fprodsplit1f  12106  fprodap0f  12108  fprodle  12112  sin02gt0  12236  efieq1re  12244  p1modz1  12266  dvdsleabs2  12318  4dvdseven  12389  bitsfzo  12427  bitsinv1lem  12433  gcdeq0  12459  rppwr  12510  uzwodc  12519  algfx  12535  eucalgcvga  12541  lcmmndc  12545  lcmeq0  12554  qredeq  12579  isprm3  12601  rpexp  12636  sqpweven  12658  2sqpwodd  12659  phicl2  12697  phibnd  12700  phiprmpw  12705  fermltl  12717  pythagtriplem4  12752  pythagtriplem6  12754  pythagtriplem7  12755  pythagtriplem12  12759  pythagtriplem13  12760  pythagtriplem14  12761  pythagtriplem16  12763  pcdvdsb  12804  pc2dvds  12814  difsqpwdvds  12822  pcmpt  12827  pcmptdvds  12829  fldivp1  12832  prmpwdvds  12839  infpnlem1  12843  1arith  12851  4sqlem11  12885  ennnfonelemk  12932  ennnfonelemhom  12947  ennnfonelemrnh  12948  ennnfonelemf1  12950  ctinf  12962  ctiunctlemudc  12969  ctiunctlemf  12970  nninfdclemp1  12982  strslfvd  13035  strslfv2d  13036  strslssd  13040  imasival  13299  imasbas  13300  imasplusg  13301  imasaddfnlemg  13307  imasaddvallemg  13308  qusaddvallemg  13326  qusaddflemg  13327  qusaddval  13328  qusaddf  13329  qusmulval  13330  qusmulf  13331  lidrididd  13375  gsumfzval  13384  sgrpidmndm  13413  gsumfzz  13488  qusgrp2  13610  mulgnegnn  13629  eqgen  13724  rinvmod  13806  gsumfzconst  13838  qusrng  13881  srgdilem  13892  ringdilem  13935  qusring2  13989  lssintclm  14307  gsumfzfsumlemm  14510  mplsubgfilemm  14621  eltg3  14690  iuncld  14748  cnss2  14860  txcnp  14904  uptx  14907  xblm  15050  metss  15127  fsumcncntop  15200  rescncf  15214  dedekindeulemlu  15254  suplociccex  15258  dedekindicclemlu  15263  dedekindicc  15266  ivthdec  15277  limccnp2lem  15309  dvaddxx  15336  dvmulxx  15337  dvrecap  15346  reeff1olem  15404  perfectlem2  15633  lgsval  15642  lgsfvalg  15643  lgsfcl2  15644  lgscllem  15645  lgsval2lem  15648  lgsneg  15662  lgsdir2  15671  lgsdir  15673  lgsdi  15675  lgsne0  15676  lgsdirnn0  15685  lgsdinn0  15686  gausslemma2dlem0c  15689  m1lgs  15723  2lgslem1  15729  2lgs  15742  2lgsoddprm  15751  2sqlem6  15758  incistruhgr  15847  upgredg  15899  uhgr2edg  15961  sumdc2  16043  pwle2  16245  subctctexmid  16247  nninfsellemeq  16261  nnnninfex  16269  exmidsbthrlem  16271  cndcap  16308