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  164  2thd  266  jca  512  syl2anc  584  unitresl  867  aevlem0  2034  equvel  2438  elex2  3462  elex22  3463  spcimdv  3537  rspcdf  3554  rspcdva  3567  elabd  3609  spsbcd  3725  opth  5267  euotd  5301  wereu2  5447  unielrel  6007  tz7.7  6099  funmo  6248  fvelimad  6607  iinpreima  6709  fnfvima  6867  resfvresima  6869  fliftfun  6935  fliftval  6939  weniso  6977  riota5f  7009  riotass2  7011  ofmpteq  7293  ssorduni  7363  suceloni  7391  nlimsucg  7420  tfisi  7436  zfrep6  7519  curry1  7662  curry2  7665  fnwelem  7685  funsssuppss  7714  wfrlem4  7816  wfrlem4OLD  7817  smogt  7863  tfrlem5  7875  omeulem1  8065  oeworde  8076  oelimcl  8083  oeeulem  8084  oeeui  8085  nnawordex  8120  oaabs2  8129  swoso  8179  qliftlem  8235  resixp  8352  undom  8459  xpdom3  8469  domunsncan  8471  omxpenlem  8472  domssex  8532  xpf1o  8533  mapdom3  8543  findcard  8610  f1dmvrnfibi  8661  fiin  8739  marypha1lem  8750  marypha1  8751  fisupcl  8786  supgtoreq  8787  ordiso2  8832  ordtypelem2  8836  ordtypelem8  8842  wemapso2lem  8869  unxpwdom2  8905  cantnflt  8988  cantnfrescl  8992  oemapvali  9000  cantnflem1d  9004  wemapwe  9013  cnfcom  9016  rankr1id  9144  tcrank  9166  cardmin2  9280  infxpenlem  9292  fseqen  9306  ween  9314  ac5num  9315  indcardi  9320  acni2  9325  fodomfi2  9339  infpwfien  9341  inffien  9342  iunfictbso  9393  acacni  9419  dfac12lem2  9423  djuinf  9467  infmap2  9493  ackbij1lem18  9512  ackbij1b  9514  fictb  9520  cfslb2n  9543  cofsmo  9544  cfsmolem  9545  coftr  9548  infpssrlem4  9581  domfin4  9586  fin2i2  9593  isfin2-2  9594  fincssdom  9598  ssfin3ds  9605  fin23lem20  9612  fin23lem30  9617  isf32lem3  9630  fin1a2lem12  9686  fin1a2lem13  9687  hsmexlem2  9702  axdc2lem  9723  imadomg  9809  fnct  9812  iundom2g  9815  iundomg  9816  iundom  9817  unirnfdomd  9842  konigthlem  9843  iunctb  9849  fpwwe2  9918  canthwelem  9925  pwfseqlem3  9935  pwfseqlem5  9938  winalim2  9971  wunelss  9983  r1wunlim  10012  wunex2  10013  tsksdom  10031  tskinf  10044  inttsk  10049  inar1  10050  tskcard  10056  tskurn  10064  gruina  10093  grur1a  10094  grur1  10095  addsrpr  10350  mulsrpr  10351  lemul12a  11352  lemulge11  11356  lediv12a  11387  nngt0  11522  nn0ge2m1nn  11818  peano5uzi  11925  nn0ind-raph  11936  znnn0nn  11948  suprzub  12192  uzsupss  12193  rpge0  12256  fz0fzelfz0  12867  fz0fzdiffz0  12870  ige2m2fzo  12954  elfzodifsumelfzo  12957  elfzom1elp1fzo  12958  fzonfzoufzol  12994  flltdivnn0lt  13057  fldiv  13082  modaddmodup  13156  uzrdgsuci  13182  fzennn  13190  uzindi  13204  fsuppmapnn0fiubex  13214  expcl2lem  13295  leexp1a  13393  modexp  13453  faclbnd  13504  faclbnd6  13513  facavg  13515  hashginv  13548  hashf1rn  13567  hasheqf1od  13568  seqcoll  13674  hashge2el2dif  13688  wrdsymb0  13751  wrdlenge2n0  13754  ccatsymb  13784  swrdnd2  13857  swrdnd0  13859  pfxnd  13889  pfxccat1  13904  swrdpfx  13909  pfxpfx  13910  wrd2ind  13925  pfxccatin12  13935  pfxccat3  13936  swrdccat  13937  pfxccatpfx1  13938  pfxccatpfx2  13939  swrdccatin1d  13945  pfxccatin12d  13947  repswswrd  13986  cshwidxmod  14005  s2f1o  14118  f1oun2prg  14119  wwlktovfo  14160  relexpreld  14237  relexpfld  14246  rtrclreclem3  14257  resqrex  14448  cau3lem  14552  reusq0  14660  rlimcld2  14773  climcn2  14787  isercoll  14862  climsup  14864  caurcvgr  14868  sumeq2ii  14887  summolem3  14908  zsum  14912  fsumadd  14933  fsum2dlem  14962  fsum0diag2  14975  fsummulc2  14976  fsumabs  14993  fsumrelem  14999  fsumrlim  15003  fsumo1  15004  o1fsum  15005  fsumiun  15013  qshash  15019  prodeq2ii  15104  prodmolem3  15124  fprodmul  15151  fproddiv  15152  fprod2dlem  15171  fprodsplit1f  15181  sin02gt0  15382  efieq1re  15389  p1modz1  15451  dvdsleabs2  15499  4dvdseven  15561  sumeven  15575  sumodd  15576  divalglem9  15589  smupvallem  15669  rppwr  15741  algfx  15757  eucalgcvga  15763  lcmfunsnlem1  15814  lcmfunsnlem2lem1  15815  lcmflefac  15825  qredeq  15834  fermltl  15954  modprm0  15975  pythagtriplem4  15989  pythagtriplem6  15991  pythagtriplem7  15992  pythagtriplem12  15996  pythagtriplem13  15997  pythagtriplem14  15998  pythagtriplem16  16000  difsqpwdvds  16056  pcmpt  16061  prmreclem2  16086  4sqlem11  16124  vdwlem9  16158  vdwlem11  16160  vdwlem12  16161  0ram  16189  0ram2  16190  0ramcl  16192  ramcl  16198  prmolelcmf  16217  cshwsidrepsw  16260  cshwshashlem2  16263  prmlem1  16274  prmlem2  16286  strfvd  16361  strfv2d  16362  strssd  16366  firest  16539  prdsdsval3  16591  imasbas  16618  imasds  16619  imasaddfnlem  16634  imasaddvallem  16635  imasvscafn  16643  qusaddvallem  16657  qusaddflem  16658  qusaddval  16659  qusaddf  16660  qusmulval  16661  qusmulf  16662  catideu  16779  idinv  16892  brcici  16903  invfuc  17077  2initoinv  17103  initoeu1w  17105  initoeu2lem0  17106  2termoinv  17110  termoeu1w  17112  mod2ile  17549  lubss  17564  acsmapd  17621  gsumval2a  17722  mndind  17809  mgm2nsgrplem4  17851  qusgrp2  17978  mulgnegnn  17997  pgrpsubgsymg  18271  fvcosymgeq  18292  gsmsymgreqlem1  18293  psgnunilem4  18360  pgpssslw  18473  sylow2alem2  18477  fislw  18484  efgsres  18595  gsumval3lem2  18751  gsumzaddlem  18765  gsum2d  18816  nn0gsumfz  18825  telgsums  18834  dprddomcld  18844  ablfac2  18932  srgi  18955  ringi  19004  qusring2  19064  lssintcl  19430  lbsextlem3  19626  lbsextlem4  19627  evlseu  19987  mptcoe1fsupp  20070  cply1coe0bi  20155  mpfpf1  20200  pf1mpf  20201  zringlpirlem3  20319  psgnodpm  20418  psgndiflemB  20430  frlmup4  20631  lindff1  20650  lindfrn  20651  lmisfree  20672  mat0dimscm  20766  mdetdiagid  20897  mdet1  20898  mdetunilem9  20917  slesolinv  20977  cramerimp  20983  cpmatmcllem  21014  mptcoe1matfsupp  21098  mp2pm2mp  21107  chpdmat  21137  cctop  21302  subbascn  21550  cnss2  21573  cmpcovf  21687  2ndcctbss  21751  2ndcomap  21754  2ndcsep  21755  comppfsc  21828  ptclsg  21911  dfac14  21914  txcnp  21916  ptcnplem  21917  uptx  21921  txtube  21936  tx2ndc  21947  xkococnlem  21955  elqtop  21993  qtoprest  22013  indishmph  22094  ptcmpfi  22109  kqhmph  22115  csdfil  22190  filssufilg  22207  ufilen  22226  rnelfm  22249  fmfnfmlem4  22253  alexsubALTlem4  22346  ptcmplem4  22351  cnextfvval  22361  cnextcn  22363  cnextfres  22365  tmdgsum2  22392  imasf1oxmet  22672  metss  22805  met2ndci  22819  prdsxmslem2  22826  metust  22855  cfilucfil  22856  metustbl  22863  psmetutop  22864  opnreen  23126  rectbntr0  23127  fsumcn  23165  rescncf  23192  xrhmeo  23237  cnllycmp  23247  lebnumlem1  23252  lebnumlem3  23254  cfilss  23560  iscmet3lem1  23581  iscmet3lem2  23582  ivthicc  23746  ovolsslem  23772  ovoliunlem2  23791  ovoliunnul  23795  ovolicc2lem4  23808  voliunlem3  23840  volsup  23844  uniiccdif  23866  uniioombllem2  23871  volivth  23895  mbfimaopnlem  23943  mbflimsup  23954  i1fd  23969  itg1addlem4  23987  itg2addlem  24046  itg2gt0  24048  limciun  24179  dvadd  24224  dvmul  24225  dvco  24231  dvrec  24239  dvcnv  24261  dvferm  24272  rollelem  24273  dvlip  24277  dvlip2  24279  c1liplem1  24280  c1lip2  24282  dvgt0lem1  24286  dvivthlem1  24292  lhop1lem  24297  dvcnvrelem1  24301  dvcnvrelem2  24302  dvcvx  24304  dvfsumle  24305  dvfsumabs  24307  dvfsumlem1  24310  dvfsumlem2  24311  dvfsumlem4  24313  dvfsumrlim2  24316  dvfsum2  24318  ftc1cn  24327  ftc2ditglem  24329  itgsubstlem  24332  tdeglem4  24341  mdegaddle  24355  mdegmullem  24359  deg1sublt  24391  ply1divmo  24416  fta1g  24448  dgrub  24511  dgrnznn  24524  dgradd2  24545  dvply1  24560  plyrem  24581  aalioulem4  24611  aalioulem5  24612  aalioulem6  24613  aaliou2  24616  taylf  24636  ulmdv  24678  psercn2  24698  abelth  24716  abelth2  24717  reeff1olem  24721  efopn  24926  logreclem  25025  isosctrlem2  25082  xrlimcnp  25232  basellem4  25347  ppiwordi  25425  musum  25454  chpub  25482  gausslemma2dlem0c  25620  2sqlem6  25685  addsqnreup  25705  2sqreulem1  25708  2sqreunnlem1  25711  dchrisumlema  25750  dchrisumlem2  25752  dchrisumlem3  25753  pntlemp  25872  pntleml  25873  ostth3  25900  iscgrglt  25986  colline  26121  axlowdimlem16  26430  axlowdimlem17  26431  axcontlem3  26439  axcontlem10  26446  uhgr2edg  26677  nbupgruvtxres  26876  cusgrres  26917  cusgrfilem2  26925  vdumgr0  26949  frusgrnn0  27040  wlklenvclwlk  27123  wlkp1lem8  27148  pthdivtx  27196  upgrwlkdvde  27204  spthonepeq  27219  usgr2pthlem  27230  lfgrn1cycl  27269  wwlknbp1  27308  wwlknllvtx  27310  wlkiswwlks2lem3  27335  umgr2adedgspth  27413  clwlkclwwlklem3  27465  clwwisshclwwslemlem  27477  clwwisshclwws  27479  wwlksubclwwlk  27523  eleclclwwlknlem1  27525  eleclclwwlknlem2  27526  erclwwlknref  27534  clwwlknonccat  27561  clwwlknonex2lem2  27573  3wlkdlem4  27627  vdn0conngrumgrv2  27661  eucrctshift  27708  frgrnbnb  27760  frgrncvvdeqlem2  27767  frgrncvvdeqlem3  27768  fusgreghash2wspv  27802  numclwwlk2lem1  27843  numclwlk2lem2f  27844  numclwwlk5  27855  numclwwlk7  27858  frgrreggt1  27860  minvecolem4b  28342  minvecolem4  28344  bcsiALT  28643  ococin  28872  spanpr  29044  pjorthi  29133  nmbdoplbi  29488  nmcoplbi  29492  nmbdfnlbi  29513  nmcfnlbi  29516  nmopcoi  29559  branmfn  29569  hstnmoc  29687  mdsl0  29774  atomli  29846  atcvat4i  29861  atabsi  29865  foresf1o  29953  rabfodom  29954  abrexdomjm  29955  elpreq  29975  ifeqeqx  29982  disjiunel  30032  fovcld  30071  aciunf1lem  30093  ffsrn  30149  xlt2addrd  30166  supxrnemnf  30177  ssnnssfz  30194  dvdszzq  30211  resspos  30316  resstos  30317  archirngz  30452  orngsqr  30527  isarchiofld  30540  locfinreflem  30717  cmpcref  30727  fmcncfil  30787  xrge0iifiso  30791  elzdif0  30834  qqhval2lem  30835  esumcst  30935  esumrnmpt2  30940  esumpinfval  30945  esumpinfsum  30949  sigaclci  31004  insiga  31009  ldgenpisys  31038  measres  31094  measdivcstALTV  31097  dya2iocnrect  31152  dya2iocnei  31153  omssubadd  31171  carsggect  31189  carsgclctunlem2  31190  sitgclg  31213  eulerpartlemsv2  31229  eulerpartlemv  31235  eulerpartlemf  31241  eulerpartlemgh  31249  eulerpartlemgs2  31251  ballotlemfp1  31362  ballotlemfrcn0  31400  ftc2re  31482  fdvposlt  31483  fdvposle  31485  bnj1379  31715  bnj580  31797  bnj944  31822  bnj999  31841  bnj1204  31894  bnj1398  31916  cusgredgex  31978  pthacycspth  32014  derangenlem  32028  subfacp1lem3  32039  subfacp1lem5  32041  resconn  32103  cvmliftlem3  32144  satfv0fvfmla0  32270  satfv1fvfmla1  32280  mrsub0  32373  frpomin  32689  frrlem4  32737  frrlem8  32741  frrlem10  32743  fprlem1  32748  fprlem2  32749  frrlem15  32753  frrlem16  32754  sltres  32780  noextenddif  32786  nolesgn2ores  32790  nosep1o  32797  nosepeq  32800  nolt02o  32810  noresle  32811  nosupno  32814  nosupres  32818  nosupbnd1lem1  32819  nosupbnd1lem4  32822  nosupbnd1  32825  nosupbnd2lem1  32826  nosupbnd2  32827  sslttr  32879  cgrextend  33080  segconeq  33082  trisegint  33100  fwddifnp1  33237  ivthALT  33294  fnessref  33316  refssfne  33317  neibastop1  33318  filnetlem4  33340  ontgval  33390  unblimceq0lem  33456  unbdqndv2lem2  33460  unbdqndv2  33461  bj-babygodel  33548  bj-spcimdv  33789  bj-spcimdvv  33790  bj-ismoored  34020  bj-finsumval0  34140  dfgcd3  34157  relowlssretop  34196  relowlpssretop  34197  onsucuni3  34200  finxpreclem4  34227  poimirlem18  34462  poimirlem21  34465  poimirlem25  34469  ftc1cnnclem  34517  ftc1cnnc  34518  ftc2nc  34528  dvasin  34530  dvacos  34531  abrexdom  34558  indexdom  34562  mettrifi  34585  equivtotbnd  34609  totbndbnd  34620  prdstotbnd  34625  heibor1lem  34640  bfplem1  34653  bfplem2  34654  opidonOLD  34683  rngodm1dm2  34763  zerdivemp1x  34778  equid1  35587  omllaw5N  35935  cmtcomlemN  35936  cmtbr3N  35942  omlfh3N  35947  atlen0  35998  exatleN  36092  hlrelat3  36100  cvrexchlem  36107  atlelt  36126  cvrat4  36131  4atlem11b  36296  4atlem12b  36299  lneq2at  36466  cdlema1N  36479  cdlemblem  36481  paddss12  36507  paddasslem2  36509  paddasslem4  36511  paddasslem6  36513  paddasslem12  36519  paddunN  36615  poml4N  36641  poml5N  36642  osumcllem6N  36649  pexmidlem6N  36663  pl42lem2N  36668  ltrnu  36809  ltrneq2  36836  trlval2  36851  cdlemd6  36891  cdleme25b  37042  cdleme29b  37063  cdlemefr29exN  37090  ltrniotacnvval  37270  cdlemk28-3  37596  dochexmidlem7  38154  qsalrel  38676  frlmsnic  38697  mzpsubmpt  38846  mzpsubst  38851  eqrabdioph  38880  rabdiophlem2  38905  elpell14qr2  38965  elpell1qr2  38975  pellfundre  38984  pellfundge  38985  pellfundglb  38988  pellfund14gap  38990  congabseq  39077  jm2.22  39098  jm2.23  39099  jm2.26lem3  39104  wepwsolem  39148  dnwech  39154  aomclem2  39161  aomclem4  39163  pwfi2f1o  39202  itgpowd  39327  ss2iundf  39510  dssmapf1od  39873  neik0pk1imk0  39903  gneispace  39990  grur1cld  40086  cpcolld  40112  mnuop23d  40120  mnuprdlem1  40126  mnuprdlem2  40127  mnurndlem1  40135  grumnudlem  40139  radcnvrat  40205  sbiota1  40325  ordelordALT  40431  2pm13.193  40446  ee11an  40584  refsumcn  40847  rfcnnnub  40853  disjxp1  40891  xrnmnfpnf  40907  ssinc  40913  nssd  40932  ralimda  40966  disjf1o  41013  disjinfi  41015  choicefi  41024  axccdom  41048  dmrelrnrel  41051  monoords  41126  fperiodmullem  41132  xadd0ge  41150  xrssre  41178  xrlexaddrp  41182  xrred  41195  infxr  41197  fiminre2  41208  xrnpnfmnf  41314  monoordxrv  41321  monoord2xrv  41323  fsumsplit1  41416  fsumiunss  41419  fmul01  41424  fmuldfeqlem1  41426  fmuldfeq  41427  fmul01lt1lem1  41428  fmul01lt1lem2  41429  cncfmptss  41431  climinf  41450  climsuselem1  41451  climsuse  41452  limcperiod  41472  limcrecl  41473  sumnnodd  41474  limcleqr  41488  0ellimcdiv  41493  climleltrp  41520  limsuppnfdlem  41545  limsupresxr  41610  liminfresxr  41611  liminfvalxr  41627  cnrefiisplem  41673  xlimmnfvlem1  41676  xlimpnfvlem1  41680  cncfperiod  41725  icccncfext  41733  cncfiooicclem1  41739  dvbdfbdioolem1  41776  dvnmptdivc  41786  dvdsn1add  41787  dvnmptconst  41789  dvnmul  41791  dvmptfprodlem  41792  dvmptfprod  41793  dvnprodlem2  41795  iblspltprt  41821  itgsubsticclem  41823  itgspltprt  41827  itgsbtaddcnst  41830  stoweidlem3  41852  stoweidlem16  41865  stoweidlem17  41866  stoweidlem19  41868  stoweidlem20  41869  stoweidlem23  41872  stoweidlem25  41874  stoweidlem27  41876  stoweidlem31  41880  stoweidlem34  41883  stoweidlem42  41891  stoweidlem48  41897  stoweidlem51  41900  stoweidlem52  41901  stoweidlem59  41908  wallispilem1  41914  wallispilem3  41916  stirlinglem13  41935  fourierdlem16  41972  fourierdlem20  41976  fourierdlem21  41977  fourierdlem38  41994  fourierdlem42  41998  fourierdlem46  42001  fourierdlem48  42003  fourierdlem49  42004  fourierdlem50  42005  fourierdlem54  42009  fourierdlem68  42023  fourierdlem72  42027  fourierdlem73  42028  fourierdlem76  42031  fourierdlem79  42034  fourierdlem81  42036  fourierdlem86  42041  fourierdlem89  42044  fourierdlem90  42045  fourierdlem91  42046  fourierdlem92  42047  fourierdlem97  42052  fourierdlem101  42056  fourierdlem103  42058  fourierdlem104  42059  fourierdlem111  42066  etransclem24  42107  etransclem25  42108  etransclem28  42111  etransclem41  42124  etransclem44  42127  etransclem48  42131  salexct  42181  dfsalgen2  42188  sge0f1o  42228  sge0rnbnd  42239  sge0split  42255  sge0iunmptlemre  42261  sge0fodjrnlem  42262  sge0iunmpt  42264  nnfoctbdjlem  42301  iundjiunlem  42305  meadjiunlem  42311  ismeannd  42313  meaiuninclem  42326  omeiunle  42363  carageniuncllem1  42367  caratheodorylem1  42372  hoidmvlelem4  42444  hoiqssbllem2  42469  salpreimagelt  42550  salpreimalegt  42552  pimdecfgtioc  42557  smfaddlem2  42604  smflimlem6  42616  nsssmfmbflem  42618  smfpimcclem  42645  or2expropbilem1  42805  funressndmfvrn  42817  2leaddle2  43036  smonoord  43069  iccpartf  43095  ich2exprop  43137  ichnreuop  43138  ichreuopeq  43139  sprbisymrel  43165  fmtnodvds  43210  proththdlem  43282  gbowgt5  43431  gboge9  43433  gbege6  43434  stgoldbwt  43445  sbgoldbalt  43450  bgoldbnnsum3prm  43473  isomgrtrlem  43507  uspgrbisymrelALT  43534  ssnn0ssfz  43897  ldepspr  44030  iunord  44281  bnd2d  44286  setrecsss  44305