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  1608  exlimd2  1618  elex22  2787  elex2  2788  spcimdv  2857  spcimedv  2859  spcedv  2862  rspcdva  2882  elabd  2918  spsbcd  3011  opth  4281  euotd  4299  ssorduni  4535  tfisi  4635  omsinds  4670  nnpredcl  4671  sotri2  5080  sotri3  5081  unielrel  5210  funmo  5286  fnfvima  5819  fliftfun  5865  fliftval  5869  riota5f  5924  riotass2  5926  fovcld  6050  oprssdmm  6257  tfrlem5  6400  tfrlemibxssdm  6413  tfrlemibfn  6414  tfrlemiex  6417  tfr1onlemsucfn  6426  tfr1onlemsucaccv  6427  tfr1onlembxssdm  6429  tfr1onlembfn  6430  tfr1onlemex  6433  tfr1onlemres  6435  tfrcllemsucfn  6439  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllembfn  6443  tfrcllemex  6446  tfrcllemres  6448  tfrcl  6450  rdgisucinc  6471  frecabex  6484  frecabcl  6485  nntr2  6589  ertr  6635  qliftlem  6700  th3q  6727  resixp  6820  f1dom2g  6847  dom3d  6865  domssr  6869  en1  6891  xpdom3m  6929  xpf1o  6941  phplem4dom  6959  phpm  6962  phpelm  6963  findcard  6985  finexdc  6999  fiintim  7028  fisseneq  7031  ssfirab  7033  opabfi  7035  f1dmvrnfibi  7046  iunfidisj  7048  fidcenumlemrk  7056  dcfi  7083  suplub2ti  7103  supelti  7104  ordiso2  7137  caseinl  7193  caseinr  7194  djudom  7195  difinfsn  7202  difinfinf  7203  ctm  7211  enumct  7217  nnnninfeq  7230  ismkvnex  7257  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  acfun  7319  exmidontriimlem2  7334  exmidontriimlem3  7335  exmidapne  7372  cc2lem  7378  cc3  7380  recexnq  7503  ltbtwnnqq  7528  addnnnq0  7562  mulnnnq0  7563  prarloclemn  7612  prarloc  7616  distrlem1prl  7695  distrlem1pru  7696  distrlem4prl  7697  distrlem4pru  7698  ltexprlemrl  7723  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  addsrpr  7858  mulsrpr  7859  map2psrprg  7918  axpre-suploclemres  8014  lemul12a  8935  lemulge11  8939  sup3exmid  9030  nngt0  9061  nn0ge0  9320  nn0ge2m1nn  9355  zletric  9416  zlelttric  9417  nn0n0n1ge2b  9452  nn0ind-raph  9490  supinfneg  9716  infsupneg  9717  infregelbex  9719  rpge0  9788  fz0fzelfz0  10249  fz0fzdiffz0  10252  ige2m2fzo  10327  elfzodifsumelfzo  10330  elfzom1elp1fzo  10331  exfzdc  10369  zsupcllemstep  10372  infssuzex  10376  qletric  10384  qlelttric  10385  rebtwn2zlemshrink  10396  frecuzrdgtcl  10557  frecuzrdg0  10558  frecuzrdgfunlem  10564  frecuzrdg0t  10567  frecuzrdgsuctlem  10568  frecfzennn  10571  seq3f1olemstep  10659  expcl2lemap  10696  leexp1a  10739  expnbnd  10808  faclbnd  10886  faclbnd6  10889  facavg  10891  fihasheqf1oi  10932  fihashf1rn  10933  fihashss  10961  fiubm  10973  seq3coll  10987  wrdsymb0  11026  wrdlenge2n0  11029  ccatsymb  11058  resqrexlemdecn  11323  qabsor  11386  cau3lem  11425  xrmaxiflemab  11558  xrmaxadd  11572  climcn2  11620  sumeq2  11670  sumrbdclem  11688  summodclem3  11691  summodclem2a  11692  zsumdc  11695  fsumgcl  11697  fsum3  11698  isumss  11702  fsumadd  11717  fsum2dlemstep  11745  fisum0diag2  11758  fsummulc2  11759  modfsummodlemstep  11768  fsumabs  11776  fsumrelem  11782  fsumiun  11788  isumshft  11801  mertenslem2  11847  prodeq2  11868  prodrbdclem  11882  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  fprodmul  11902  fprodconst  11931  fprodap0  11932  fprod2dlemstep  11933  fprodrec  11940  fprodsplit1f  11945  fprodap0f  11947  fprodle  11951  sin02gt0  12075  efieq1re  12083  p1modz1  12105  dvdsleabs2  12157  4dvdseven  12228  bitsfzo  12266  bitsinv1lem  12272  gcdeq0  12298  rppwr  12349  uzwodc  12358  algfx  12374  eucalgcvga  12380  lcmmndc  12384  lcmeq0  12393  qredeq  12418  isprm3  12440  rpexp  12475  sqpweven  12497  2sqpwodd  12498  phicl2  12536  phibnd  12539  phiprmpw  12544  fermltl  12556  pythagtriplem4  12591  pythagtriplem6  12593  pythagtriplem7  12594  pythagtriplem12  12598  pythagtriplem13  12599  pythagtriplem14  12600  pythagtriplem16  12602  pcdvdsb  12643  pc2dvds  12653  difsqpwdvds  12661  pcmpt  12666  pcmptdvds  12668  fldivp1  12671  prmpwdvds  12678  infpnlem1  12682  1arith  12690  4sqlem11  12724  ennnfonelemk  12771  ennnfonelemhom  12786  ennnfonelemrnh  12787  ennnfonelemf1  12789  ctinf  12801  ctiunctlemudc  12808  ctiunctlemf  12809  nninfdclemp1  12821  strslfvd  12874  strslfv2d  12875  strslssd  12879  imasival  13138  imasbas  13139  imasplusg  13140  imasaddfnlemg  13146  imasaddvallemg  13147  qusaddvallemg  13165  qusaddflemg  13166  qusaddval  13167  qusaddf  13168  qusmulval  13169  qusmulf  13170  lidrididd  13214  gsumfzval  13223  sgrpidmndm  13252  gsumfzz  13327  qusgrp2  13449  mulgnegnn  13468  eqgen  13563  rinvmod  13645  gsumfzconst  13677  qusrng  13720  srgdilem  13731  ringdilem  13774  qusring2  13828  lssintclm  14146  gsumfzfsumlemm  14349  mplsubgfilemm  14460  eltg3  14529  iuncld  14587  cnss2  14699  txcnp  14743  uptx  14746  xblm  14889  metss  14966  fsumcncntop  15039  rescncf  15053  dedekindeulemlu  15093  suplociccex  15097  dedekindicclemlu  15102  dedekindicc  15105  ivthdec  15116  limccnp2lem  15148  dvaddxx  15175  dvmulxx  15176  dvrecap  15185  reeff1olem  15243  perfectlem2  15472  lgsval  15481  lgsfvalg  15482  lgsfcl2  15483  lgscllem  15484  lgsval2lem  15487  lgsneg  15501  lgsdir2  15510  lgsdir  15512  lgsdi  15514  lgsne0  15515  lgsdirnn0  15524  lgsdinn0  15525  gausslemma2dlem0c  15528  m1lgs  15562  2lgslem1  15568  2lgs  15581  2lgsoddprm  15590  2sqlem6  15597  sumdc2  15735  pwle2  15935  subctctexmid  15937  nninfsellemeq  15951  nnnninfex  15959  exmidsbthrlem  15961  cndcap  15998