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  2816  elex2  2817  spcimdv  2888  spcimedv  2890  spcedv  2893  rspcdva  2913  elabd  2949  spsbcd  3042  opth  4327  euotd  4345  ssorduni  4583  tfisi  4683  omsinds  4718  nnpredcl  4719  sotri2  5132  sotri3  5133  unielrel  5262  funmo  5339  fnfvima  5884  resfvresima  5886  fliftfun  5932  fliftval  5936  riota5f  5993  riotass2  5995  fovcld  6121  oprssdmm  6329  tfrlem5  6475  tfrlemibxssdm  6488  tfrlemibfn  6489  tfrlemiex  6492  tfr1onlemsucfn  6501  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemex  6508  tfr1onlemres  6510  tfrcllemsucfn  6514  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemex  6521  tfrcllemres  6523  tfrcl  6525  rdgisucinc  6546  frecabex  6559  frecabcl  6560  nntr2  6666  ertr  6712  qliftlem  6777  th3q  6804  resixp  6897  f1dom2g  6924  dom3d  6942  domssr  6946  en1  6968  xpdom3m  7013  xpf1o  7025  phplem4dom  7043  phpm  7047  phpelm  7048  findcard  7070  finexdc  7085  fiintim  7116  fisseneq  7119  ssfirab  7121  opabfi  7123  f1dmvrnfibi  7134  iunfidisj  7136  fidcenumlemrk  7144  dcfi  7171  suplub2ti  7191  supelti  7192  ordiso2  7225  caseinl  7281  caseinr  7282  djudom  7283  difinfsn  7290  difinfinf  7291  ctm  7299  enumct  7305  nnnninfeq  7318  ismkvnex  7345  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  acfun  7412  exmidontriimlem2  7427  exmidontriimlem3  7428  exmidapne  7469  cc2lem  7475  cc3  7477  recexnq  7600  ltbtwnnqq  7625  addnnnq0  7659  mulnnnq0  7660  prarloclemn  7709  prarloc  7713  distrlem1prl  7792  distrlem1pru  7793  distrlem4prl  7794  distrlem4pru  7795  ltexprlemrl  7820  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  addsrpr  7955  mulsrpr  7956  map2psrprg  8015  axpre-suploclemres  8111  lemul12a  9032  lemulge11  9036  sup3exmid  9127  nngt0  9158  nn0ge0  9417  nn0ge2m1nn  9452  zletric  9513  zlelttric  9514  nn0n0n1ge2b  9549  nn0ind-raph  9587  supinfneg  9819  infsupneg  9820  infregelbex  9822  rpge0  9891  fz0fzelfz0  10352  fz0fzdiffz0  10355  ige2m2fzo  10433  elfzodifsumelfzo  10436  elfzom1elp1fzo  10437  exfzdc  10476  zsupcllemstep  10479  infssuzex  10483  qletric  10491  qlelttric  10492  rebtwn2zlemshrink  10503  frecuzrdgtcl  10664  frecuzrdg0  10665  frecuzrdgfunlem  10671  frecuzrdg0t  10674  frecuzrdgsuctlem  10675  frecfzennn  10678  seq3f1olemstep  10766  expcl2lemap  10803  leexp1a  10846  expnbnd  10915  faclbnd  10993  faclbnd6  10996  facavg  10998  fihasheqf1oi  11039  fihashf1rn  11040  fihashss  11070  fiubm  11082  seq3coll  11096  wrdsymb0  11136  wrdlenge2n0  11139  ccatsymb  11169  pfxnd  11260  pfxccat1  11273  swrdpfx  11278  pfxpfx  11279  wrd2ind  11294  pfxccatin12  11304  pfxccat3  11305  swrdccat  11306  pfxccatpfx1  11307  pfxccatpfx2  11308  swrdccatin1d  11314  pfxccatin12d  11316  resqrexlemdecn  11563  qabsor  11626  cau3lem  11665  xrmaxiflemab  11798  xrmaxadd  11812  climcn2  11860  sumeq2  11910  sumrbdclem  11928  summodclem3  11931  summodclem2a  11932  zsumdc  11935  fsumgcl  11937  fsum3  11938  isumss  11942  fsumadd  11957  fsum2dlemstep  11985  fisum0diag2  11998  fsummulc2  11999  modfsummodlemstep  12008  fsumabs  12016  fsumrelem  12022  fsumiun  12028  isumshft  12041  mertenslem2  12087  prodeq2  12108  prodrbdclem  12122  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  fprodmul  12142  fprodconst  12171  fprodap0  12172  fprod2dlemstep  12173  fprodrec  12180  fprodsplit1f  12185  fprodap0f  12187  fprodle  12191  sin02gt0  12315  efieq1re  12323  p1modz1  12345  dvdsleabs2  12397  4dvdseven  12468  bitsfzo  12506  bitsinv1lem  12512  gcdeq0  12538  rppwr  12589  uzwodc  12598  algfx  12614  eucalgcvga  12620  lcmmndc  12624  lcmeq0  12633  qredeq  12658  isprm3  12680  rpexp  12715  sqpweven  12737  2sqpwodd  12738  phicl2  12776  phibnd  12779  phiprmpw  12784  fermltl  12796  pythagtriplem4  12831  pythagtriplem6  12833  pythagtriplem7  12834  pythagtriplem12  12838  pythagtriplem13  12839  pythagtriplem14  12840  pythagtriplem16  12842  pcdvdsb  12883  pc2dvds  12893  difsqpwdvds  12901  pcmpt  12906  pcmptdvds  12908  fldivp1  12911  prmpwdvds  12918  infpnlem1  12922  1arith  12930  4sqlem11  12964  ennnfonelemk  13011  ennnfonelemhom  13026  ennnfonelemrnh  13027  ennnfonelemf1  13029  ctinf  13041  ctiunctlemudc  13048  ctiunctlemf  13049  nninfdclemp1  13061  strslfvd  13114  strslfv2d  13115  strslssd  13119  imasival  13379  imasbas  13380  imasplusg  13381  imasaddfnlemg  13387  imasaddvallemg  13388  qusaddvallemg  13406  qusaddflemg  13407  qusaddval  13408  qusaddf  13409  qusmulval  13410  qusmulf  13411  lidrididd  13455  gsumfzval  13464  sgrpidmndm  13493  gsumfzz  13568  qusgrp2  13690  mulgnegnn  13709  eqgen  13804  rinvmod  13886  gsumfzconst  13918  qusrng  13961  srgdilem  13972  ringdilem  14015  qusring2  14069  lssintclm  14388  gsumfzfsumlemm  14591  mplsubgfilemm  14702  eltg3  14771  iuncld  14829  cnss2  14941  txcnp  14985  uptx  14988  xblm  15131  metss  15208  fsumcncntop  15281  rescncf  15295  dedekindeulemlu  15335  suplociccex  15339  dedekindicclemlu  15344  dedekindicc  15347  ivthdec  15358  limccnp2lem  15390  dvaddxx  15417  dvmulxx  15418  dvrecap  15427  reeff1olem  15485  perfectlem2  15714  lgsval  15723  lgsfvalg  15724  lgsfcl2  15725  lgscllem  15726  lgsval2lem  15729  lgsneg  15743  lgsdir2  15752  lgsdir  15754  lgsdi  15756  lgsne0  15757  lgsdirnn0  15766  lgsdinn0  15767  gausslemma2dlem0c  15770  m1lgs  15804  2lgslem1  15810  2lgs  15823  2lgsoddprm  15832  2sqlem6  15839  incistruhgr  15931  upgredg  15983  uhgr2edg  16045  usgriedgdomord  16064  wlkpropg  16121  wlkvtxeledgg  16141  wlk2f  16148  clwwlknonccat  16228  clwwlknonex2lem2  16233  sumdc2  16331  pwle2  16535  subctctexmid  16537  nninfsellemeq  16552  nnnninfex  16560  exmidsbthrlem  16562  cndcap  16599