Theorem sylc 65

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 40	. 2 ⊢ (𝜑 → (𝜑 → 𝜃))
5	4	pm2.43i 52	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  66  mpsyl  68  jc  160  2thd  256  jca  503  syl2anc  575  syl2an23anOLD  1540  aevlem0  2149  nfimdOLD  2402  equvel  2507  elex2  3417  elex22  3418  spcimdv  3490  rspcdva  3515  elabd  3554  spsbcd  3654  opth  5141  euotd  5175  wereu2  5315  unielrel  5881  tz7.7  5969  funmo  6120  iinpreima  6570  resfvresima  6722  fnfvima  6724  fliftfun  6789  fliftval  6793  weniso  6831  riota5f  6863  riotass2  6865  ofmpteq  7149  ssorduni  7218  suceloni  7246  nlimsucg  7275  tfisi  7291  zfrep6  7367  curry1  7506  curry2  7509  fnwelem  7529  funsssuppss  7559  wfrlem4  7656  wfrlem4OLD  7657  wfrlem15  7668  smogt  7703  tfrlem5  7715  omeulem1  7902  oeworde  7913  oelimcl  7920  oeeulem  7921  oeeui  7922  nnawordex  7957  oaabs2  7965  ertr  7997  swoso  8015  qliftlem  8066  resixp  8183  f1dom2g  8213  dom3d  8237  undom  8290  xpdom3  8300  domunsncan  8302  omxpenlem  8303  disjenex  8360  domssex2  8362  domssex  8363  xpf1o  8364  mapdom3  8374  findcard  8441  f1dmvrnfibi  8492  fiin  8570  marypha1lem  8581  marypha1  8582  fisupcl  8617  supgtoreq  8618  ordiso2  8662  ordtypelem2  8666  ordtypelem8  8672  wemapso2lem  8699  brwdom2  8720  unxpwdom2  8735  cantnflt  8819  cantnfrescl  8823  oemapvali  8831  cantnflem1d  8835  wemapwe  8844  cnfcom  8847  rankr1id  8975  tcrank  8997  cardmin2  9110  infxpenlem  9122  infxpenc2lem2  9129  fseqen  9136  dfac8clem  9141  ween  9144  ac5num  9145  indcardi  9150  acni2  9155  acnlem  9157  fodomfi2  9169  infpwfien  9171  inffien  9172  finnisoeu  9222  iunfictbso  9223  acacni  9250  dfac12lem2  9254  infpss  9327  infmap2  9328  ackbij1lem18  9347  ackbij1b  9349  fictb  9355  cfslb2n  9378  cofsmo  9379  cfsmolem  9380  coftr  9383  infpssrlem4  9416  domfin4  9421  fin2i2  9428  isfin2-2  9429  fincssdom  9433  ssfin3ds  9440  fin23lem20  9447  fin23lem30  9452  isf32lem3  9465  fin1a2lem12  9521  fin1a2lem13  9522  hsmexlem2  9537  axdc2lem  9558  axdc4lem  9565  ac6num  9589  axdclem2  9630  imadomg  9644  fnct  9647  iundom2g  9650  iundomg  9651  iundom  9652  unirnfdomd  9677  konigthlem  9678  iunctb  9684  fpwwe2  9753  canthwelem  9760  pwfseqlem3  9770  pwfseqlem5  9773  winalim2  9806  wunelss  9818  r1wunlim  9847  wunex2  9848  tsksdom  9866  tskinf  9879  inttsk  9884  inar1  9885  tskcard  9891  tskurn  9899  gruina  9928  grur1a  9929  grur1  9930  addsrpr  10184  mulsrpr  10185  lemul12a  11169  lemulge11  11173  lediv12a  11204  nngt0  11338  nn0ge2m1nn  11629  peano5uzi  11735  nn0ind-raph  11746  znnn0nn  11758  suprzub  12001  uzsupss  12002  rpge0  12062  fz0fzelfz0  12672  fz0fzdiffz0  12675  ige2m2fzo  12758  elfzodifsumelfzo  12761  elfzom1elp1fzo  12762  fzonfzoufzol  12798  flltdivnn0lt  12861  fldiv  12886  modaddmodup  12960  uzrdgsuci  12986  fzennn  12994  uzindi  13008  fsuppmapnn0fiubex  13018  expcl2lem  13098  leexp1a  13145  modexp  13225  faclbnd  13300  faclbnd6  13309  facavg  13311  hashginv  13344  hashf1rn  13364  hasheqf1od  13365  fz1isolem  13465  seqcoll  13468  hashge2el2dif  13482  wrdsymb0  13553  wrdlenge2n0  13556  ccatsymb  13582  swrdnd2  13660  swrdswrd0  13689  swrd0swrd0  13690  wrd2ind  13704  swrdccatin12  13718  swrdccat3  13719  swrdccat  13720  swrdccatid  13724  swrdccatin1d  13726  swrdccatin12d  13728  repswswrd  13758  cshwidxmod  13776  s2f1o  13888  f1oun2prg  13889  wwlktovfo  13929  wrd2f1tovbij  13931  relexpreld  14006  relexpfld  14015  rtrclreclem3  14026  resqrex  14217  cau3lem  14320  rlimcld2  14535  climcn2  14549  isercoll  14624  climsup  14626  caurcvgr  14630  sumeq2ii  14649  summolem3  14671  zsum  14675  fsum  14677  fsumadd  14696  fsum2dlem  14727  fsum0diag2  14740  fsummulc2  14741  fsumabs  14758  fsumrelem  14764  fsumrlim  14768  fsumo1  14769  o1fsum  14770  fsumiun  14778  qshash  14784  ntrivcvgn0  14854  prodeq2ii  14867  prodmolem3  14887  fprod  14895  fprodcllemf  14912  fprodmul  14914  fproddiv  14915  fprod2dlem  14934  fprodsplit1f  14944  sin01gt0  15143  sin02gt0  15145  efieq1re  15152  p1modz1  15213  dvdsleabs2  15260  4dvdseven  15332  sumeven  15333  sumodd  15334  divalglem9  15347  smupvallem  15427  rppwr  15499  algfx  15515  eucalgcvga  15521  lcmfunsnlem1  15572  lcmfunsnlem2lem1  15573  lcmflefac  15583  qredeq  15592  fermltl  15709  modprm0  15730  pythagtriplem4  15744  pythagtriplem6  15746  pythagtriplem7  15747  pythagtriplem12  15751  pythagtriplem13  15752  pythagtriplem14  15753  pythagtriplem16  15755  difsqpwdvds  15811  pcmpt  15816  prmreclem2  15841  4sqlem11  15879  vdwlem9  15913  vdwlem11  15915  vdwlem12  15916  0ram  15944  0ram2  15945  0ramcl  15947  ramcl  15953  prmolelcmf  15972  cshwsidrepsw  16015  cshwshashlem2  16018  prmlem1  16029  prmlem2  16041  strfvd  16118  strfv2d  16119  strssd  16123  firest  16301  prdsdsval3  16353  imasbas  16380  imasds  16381  imasaddfnlem  16396  imasaddvallem  16397  imasvscafn  16405  qusaddvallem  16419  qusaddflem  16420  qusaddval  16421  qusaddf  16422  qusmulval  16423  qusmulf  16424  isacs1i  16525  mreacs  16526  catideu  16543  idinv  16656  brcici  16667  invfuc  16841  2initoinv  16867  initoeu1w  16869  initoeu2lem0  16870  2termoinv  16874  termoeu1w  16876  mod2ile  17314  lubss  17329  acsmapd  17386  gsumval2a  17487  mrcmndind  17574  mgm2nsgrplem4  17616  qusgrp2  17741  mulgnegnn  17759  pgrpsubgsymg  18032  fvcosymgeq  18053  gsmsymgreqlem1  18054  psgnunilem4  18121  pgpssslw  18233  sylow2alem2  18237  fislw  18244  efgsres  18355  gsumval3lem2  18511  gsumzaddlem  18525  gsum2d  18575  nn0gsumfz  18584  telgsums  18595  dprddomcld  18605  ablfac2  18693  srgi  18716  ringi  18765  qusring2  18825  lssintcl  19174  lbsextlem3  19372  lbsextlem4  19373  evlslem3  19725  evlseu  19727  mptcoe1fsupp  19796  cply1coe0bi  19881  mpfpf1  19926  pf1mpf  19927  zringlpirlem3  20045  psgnodpm  20144  psgndiflemB  20157  frlmup4  20354  lindff1  20373  lindfrn  20374  lmisfree  20395  mat0dimscm  20490  mdetdiagid  20621  mdet1  20622  mdetunilem9  20641  slesolinv  20702  cramerimp  20709  cpmatmcllem  20740  mptcoe1matfsupp  20824  mp2pm2mp  20833  chpdmat  20863  eltg3  20984  cctop  21028  subbascn  21276  cnss2  21299  cmpcovf  21412  2ndcctbss  21476  2ndcomap  21479  2ndcsep  21480  comppfsc  21553  elptr  21594  ptclsg  21636  dfac14  21639  txcnp  21641  ptcnplem  21642  uptx  21646  txtube  21661  tx2ndc  21672  xkococnlem  21680  elqtop  21718  qtoprest  21738  indishmph  21819  ptcmpfi  21834  kqhmph  21840  csdfil  21915  filssufilg  21932  ufilen  21951  rnelfm  21974  fmfnfmlem4  21978  alexsubALTlem4  22071  ptcmplem4  22076  cnextfvval  22086  cnextcn  22088  tmdgsum2  22117  imasf1oxmet  22397  metss  22530  met2ndci  22544  prdsxmslem2  22551  metust  22580  cfilucfil  22581  metustbl  22588  psmetutop  22589  opnreen  22851  rectbntr0  22852  fsumcn  22890  rescncf  22917  xrhmeo  22962  cnllycmp  22972  lebnumlem1  22977  lebnumlem3  22979  cfilss  23285  iscmet3lem1  23306  iscmet3lem2  23307  ivthicc  23445  ovolsslem  23471  ovoliunlem2  23490  ovoliunnul  23494  ovolicc2lem4  23507  voliunlem3  23539  volsup  23543  uniiccdif  23565  uniioombllem2  23570  volivth  23594  mbfimaopnlem  23642  mbflimsup  23653  i1fd  23668  itg1addlem4  23686  itg2addlem  23745  itg2gt0  23747  limciun  23878  dvadd  23923  dvmul  23924  dvco  23930  dvrec  23938  dvcnv  23960  dvferm  23971  rollelem  23972  dvlip  23976  dvlip2  23978  c1liplem1  23979  c1lip2  23981  dvgt0lem1  23985  dvivthlem1  23991  lhop1lem  23996  dvcnvrelem1  24000  dvcnvrelem2  24001  dvcvx  24003  dvfsumle  24004  dvfsumabs  24006  dvfsumlem1  24009  dvfsumlem2  24010  dvfsumlem4  24012  dvfsumrlim2  24015  dvfsum2  24017  ftc1cn  24026  ftc2ditglem  24028  itgsubstlem  24031  tdeglem4  24040  mdegaddle  24054  mdegmullem  24058  deg1sublt  24090  ply1divmo  24115  fta1g  24147  dgrub  24210  dgrnznn  24223  dgradd2  24244  dvply1  24259  plyrem  24280  aalioulem4  24310  aalioulem5  24311  aalioulem6  24312  aaliou2  24315  taylf  24335  ulmdv  24377  psercn2  24397  abelth  24415  abelth2  24416  reeff1olem  24420  efopn  24624  logreclem  24720  isosctrlem2  24769  xrlimcnp  24915  basellem4  25030  ppiwordi  25108  musum  25137  chpub  25165  gausslemma2dlem0c  25303  2sqlem6  25368  dchrisumlema  25397  dchrisumlem2  25399  dchrisumlem3  25400  dchrisum0re  25422  pntlemp  25519  pntleml  25520  ostth3  25547  colline  25764  axlowdimlem16  26057  axlowdimlem17  26058  axcontlem3  26066  axcontlem10  26073  basvtxvalOLD  26123  edgfiedgvalOLD  26124  uhgr2edg  26321  nbusgrf1o1  26494  nbupgruvtxres  26536  cusgrexg  26574  cusgrres  26578  cusgrfilem2  26586  cusgrfilem3  26587  sizusglecusg  26593  vdumgr0  26610  frusgrnn0  26701  wlklenvclwlk  26785  wlkp1lem8  26811  pthdivtx  26859  upgrwlkdvde  26867  spthonepeq  26882  usgr2pthlem  26893  lfgrn1cycl  26932  wwlknbp1  26971  wwlknllvtx  26974  wlkiswwlks2lem3  27004  umgr2adedgspth  27094  clwlkclwwlklem3  27150  clwwisshclwwslemlem  27162  clwwisshclwws  27164  wwlksubclwwlk  27215  eleclclwwlknlem1  27217  eleclclwwlknlem2  27218  erclwwlknref  27226  clwlksfclwwlkOLD  27242  clwlksf1clwwlklemOLD  27248  clwwlknonccat  27270  clwwlknonex2lem2  27283  3wlkdlem4  27341  vdn0conngrumgrv2  27375  eucrctshift  27422  frgrnbnb  27474  frgrncvvdeqlem2  27481  frgrncvvdeqlem3  27482  fusgreghash2wspv  27516  numclwwlk2lem1  27562  numclwlk2lem2f  27563  numclwwlk2lem1OLD  27569  numclwlk2lem2fOLD  27570  numclwwlk5  27582  numclwwlk7  27585  frgrreggt1  27587  minvecolem4b  28068  minvecolem4  28070  bcsiALT  28370  ococin  28601  spanpr  28773  pjorthi  28862  nmbdoplbi  29217  nmcoplbi  29221  nmbdfnlbi  29242  nmcfnlbi  29245  nmopcoi  29288  branmfn  29298  hstnmoc  29416  mdsl0  29503  atomli  29575  atcvat4i  29590  atabsi  29594  foresf1o  29674  rabfodom  29675  abrexdomjm  29676  elpreq  29691  ifeqeqx  29692  disjiunel  29740  fovcld  29773  aciunf1lem  29795  ffsrn  29837  xlt2addrd  29856  supxrnemnf  29867  ssnnssfz  29882  resspos  29990  resstos  29991  archirngz  30074  orngsqr  30135  isarchiofld  30148  locfinreflem  30238  cmpcref  30248  fmcncfil  30308  xrge0iifiso  30312  elzdif0  30355  qqhval2lem  30356  esumcst  30456  esumrnmpt2  30461  esumpinfval  30466  esumpinfsum  30470  sigaclci  30526  insiga  30531  ldgenpisys  30560  measres  30616  measdivcstOLD  30618  mbfmcnvima  30650  dya2iocnrect  30674  dya2iocnei  30675  omssubadd  30693  carsggect  30711  carsgclctunlem2  30712  sitgclg  30735  eulerpartlemsv2  30751  eulerpartlemv  30757  eulerpartlemf  30763  eulerpartlemgh  30771  eulerpartlemgs2  30773  ballotlemfp1  30884  ballotlemfrcn0  30922  ftc2re  31007  fdvposlt  31008  fdvposle  31010  bnj1379  31229  bnj580  31311  bnj944  31336  bnj999  31355  bnj1204  31408  bnj1398  31430  derangenlem  31481  subfacp1lem3  31492  subfacp1lem5  31494  resconn  31556  cvmliftlem3  31597  mrsub0  31741  frpomin  32064  frrlem4  32109  frrlem11  32118  sltres  32141  noextenddif  32147  nolesgn2ores  32151  nosep1o  32158  nosepeq  32161  nolt02o  32171  noresle  32172  nosupno  32175  nosupres  32179  nosupbnd1lem1  32180  nosupbnd1lem4  32183  nosupbnd1  32186  nosupbnd2lem1  32187  nosupbnd2  32188  sslttr  32240  cgrextend  32441  segconeq  32443  trisegint  32461  fwddifnp1  32598  ivthALT  32656  fnessref  32678  refssfne  32679  neibastop1  32680  filnetlem4  32702  ontgval  32752  unblimceq0lem  32819  unbdqndv2lem2  32823  unbdqndv2  32824  bj-babygodel  32908  bj-spcimdv  33194  bj-spcimdvv  33195  bj-ismoored  33375  bj-finsumval0  33466  dfgcd3  33489  relowlssretop  33529  relowlpssretop  33530  onsucuni3  33533  finxpreclem4  33549  poimirlem18  33742  poimirlem21  33745  poimirlem25  33749  ftc1cnnclem  33797  ftc1cnnc  33798  ftc2nc  33808  dvasin  33810  dvacos  33811  abrexdom  33839  indexdom  33843  mettrifi  33866  equivtotbnd  33890  totbndbnd  33901  prdstotbnd  33906  heibor1lem  33921  bfplem1  33934  bfplem2  33935  opidonOLD  33964  rngodm1dm2  34044  zerdivemp1x  34059  unitresl  34197  equid1  34680  omllaw5N  35029  cmtcomlemN  35030  cmtbr3N  35036  omlfh3N  35041  atlen0  35092  exatleN  35186  hlrelat3  35194  cvrexchlem  35201  atlelt  35220  cvrat4  35225  4atlem11b  35390  4atlem12b  35393  lneq2at  35560  cdlema1N  35573  cdlemblem  35575  paddss12  35601  paddasslem2  35603  paddasslem4  35605  paddasslem6  35607  paddasslem12  35613  paddunN  35709  poml4N  35735  poml5N  35736  osumcllem6N  35743  pexmidlem6N  35757  pl42lem2N  35762  ltrnu  35903  ltrneq2  35930  trlval2  35945  cdlemd6  35985  cdleme25b  36136  cdleme29b  36157  cdlemefr29exN  36184  ltrniotacnvval  36364  cdlemk28-3  36690  dochexmidlem7  37248  mzpsubmpt  37809  mzpsubst  37814  eqrabdioph  37844  rabdiophlem2  37869  elpell14qr2  37929  elpell1qr2  37939  pellfundre  37948  pellfundge  37949  pellfundglb  37952  pellfund14gap  37954  congabseq  38043  jm2.22  38064  jm2.23  38065  jm2.26lem3  38070  wepwsolem  38114  dnwech  38120  aomclem2  38127  aomclem4  38129  pwfi2f1o  38168  itgpowd  38301  ss2iundf  38452  relexpmulg  38503  dssmapf1od  38816  neik0pk1imk0  38846  gneispace  38933  radcnvrat  39014  sbiota1  39135  ordelordALT  39246  2pm13.193  39267  ee11an  39414  refsumcn  39684  rfcnnnub  39690  disjxp1  39732  xrnmnfpnf  39750  ssinc  39758  nssd  39781  ralimda  39818  disjf1o  39868  disjinfi  39870  choicefi  39880  axccdom  39904  dmrelrnrel  39907  fvelimad  39943  fnfvimad  39944  monoords  39993  fperiodmullem  39999  xadd0ge  40017  xrssre  40045  xrlexaddrp  40049  xrred  40062  infxr  40064  fiminre2  40075  xrnpnfmnf  40185  monoordxrv  40192  monoord2xrv  40194  fsumsplit1  40285  fsumiunss  40288  fmul01  40293  fmuldfeqlem1  40295  fmuldfeq  40296  fmul01lt1lem1  40297  fmul01lt1lem2  40298  cncfmptss  40300  climinf  40319  climsuselem1  40320  climsuse  40321  limcperiod  40341  limcrecl  40342  sumnnodd  40343  limcleqr  40357  0ellimcdiv  40362  climleltrp  40389  limsuppnfdlem  40414  limsupresxr  40479  liminfresxr  40480  liminfvalxr  40496  cnrefiisplem  40536  xlimmnfvlem1  40539  xlimpnfvlem1  40543  cncfperiod  40573  icccncfext  40581  cncfiooicclem1  40587  dvbdfbdioolem1  40624  dvnmptdivc  40634  dvdsn1add  40635  dvnmptconst  40637  dvnmul  40639  dvmptfprodlem  40640  dvmptfprod  40641  dvnprodlem2  40643  iblspltprt  40669  itgsubsticclem  40671  itgspltprt  40675  itgsbtaddcnst  40678  stoweidlem3  40700  stoweidlem16  40713  stoweidlem17  40714  stoweidlem19  40716  stoweidlem20  40717  stoweidlem23  40720  stoweidlem25  40722  stoweidlem27  40724  stoweidlem31  40728  stoweidlem34  40731  stoweidlem42  40739  stoweidlem48  40745  stoweidlem51  40748  stoweidlem52  40749  stoweidlem59  40756  wallispilem1  40762  wallispilem3  40764  stirlinglem13  40783  fourierdlem16  40820  fourierdlem20  40824  fourierdlem21  40825  fourierdlem38  40842  fourierdlem42  40846  fourierdlem46  40849  fourierdlem48  40851  fourierdlem49  40852  fourierdlem50  40853  fourierdlem54  40857  fourierdlem68  40871  fourierdlem72  40875  fourierdlem73  40876  fourierdlem76  40879  fourierdlem79  40882  fourierdlem81  40884  fourierdlem86  40889  fourierdlem89  40892  fourierdlem90  40893  fourierdlem91  40894  fourierdlem92  40895  fourierdlem97  40900  fourierdlem101  40904  fourierdlem103  40906  fourierdlem104  40907  fourierdlem111  40914  etransclem24  40955  etransclem25  40956  etransclem28  40959  etransclem41  40972  etransclem44  40975  etransclem48  40979  salexct  41032  dfsalgen2  41039  sge0f1o  41079  sge0rnbnd  41090  sge0split  41106  sge0iunmptlemre  41112  sge0fodjrnlem  41113  sge0iunmpt  41115  nnfoctbdjlem  41152  iundjiunlem  41156  meadjiunlem  41162  ismeannd  41164  meaiuninclem  41177  omeiunle  41214  carageniuncllem1  41218  caratheodorylem1  41223  hoidmvlelem4  41295  hoiqssbllem2  41320  salpreimagelt  41401  salpreimalegt  41403  pimdecfgtioc  41408  smfaddlem2  41455  smflimlem6  41467  nsssmfmbflem  41469  smfpimcclem  41496  funressndmfvrn  41664  2leaddle2  41889  smonoord  41917  iccpartf  41943  pfxnd  41971  pfxccat1  41986  pfxpfx  41991  pfxccatin12  42001  pfxccat3  42002  pfxccatpfx1  42003  pfxccatpfx2  42004  pfxccatin12d  42008  fmtnodvds  42032  proththdlem  42106  gbowgt5  42226  gboge9  42228  gbege6  42229  stgoldbwt  42240  sbgoldbalt  42245  bgoldbnnsum3prm  42268  sprbisymrel  42318  uspgrbisymrelALT  42332  ssnn0ssfz  42696  ldepspr  42831  iunord  42991  rspcdf  42993  bnd2d  42997  setrecsss  43016