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  161  jcnd  163  2thd  264  jca  511  syl2anc  583  unitreslOLD  874  aevlem0  2058  equvel  2456  ralimda  3421  elex2  3443  elex22  3444  spcedv  3527  rspcdf  3538  rspcdva  3554  spsbcd  3725  opth  5385  euotd  5421  wereu2  5577  unielrel  6166  frpomin  6228  tz7.7  6277  funmo  6434  fvelimad  6818  iinpreima  6928  fnfvima  7091  resfvresima  7093  fliftfun  7163  fliftval  7167  weniso  7205  riota5f  7241  riotass2  7243  ofmpteq  7533  ssorduni  7606  suceloni  7635  nlimsucg  7664  tfisi  7680  zfrep6  7771  curry1  7915  curry2  7918  fnwelem  7943  funsssuppss  7977  frrlem4  8076  frrlem8  8080  frrlem10  8082  fprlem1  8087  fprlem2  8088  wfrlem4OLD  8114  smogt  8169  tfrlem5  8182  omeulem1  8375  oeworde  8386  oelimcl  8393  oeeulem  8394  oeeui  8395  nnawordex  8430  oaabs2  8439  swoso  8489  qliftlem  8545  resixp  8679  undom  8800  xpdom3  8810  domunsncan  8812  omxpenlem  8813  domssex  8874  xpf1o  8875  mapdom3  8885  findcard  8908  f1dmvrnfibi  9033  fiin  9111  marypha1lem  9122  marypha1  9123  fisupcl  9158  supgtoreq  9159  ordiso2  9204  ordtypelem2  9208  ordtypelem8  9214  wemapso2lem  9241  unxpwdom2  9277  cantnflt  9360  cantnfrescl  9364  oemapvali  9372  cantnflem1d  9376  wemapwe  9385  cnfcom  9388  frrlem15  9446  frrlem16  9447  rankr1id  9551  tcrank  9573  cardmin2  9688  infxpenlem  9700  fseqen  9714  ween  9722  ac5num  9723  indcardi  9728  acni2  9733  fodomfi2  9747  infpwfien  9749  inffien  9750  iunfictbso  9801  acacni  9827  dfac12lem2  9831  djuinf  9875  infmap2  9905  ackbij1lem18  9924  ackbij1b  9926  fictb  9932  cfslb2n  9955  cofsmo  9956  cfsmolem  9957  coftr  9960  infpssrlem4  9993  domfin4  9998  fin2i2  10005  isfin2-2  10006  fincssdom  10010  ssfin3ds  10017  fin23lem20  10024  fin23lem30  10029  isf32lem3  10042  fin1a2lem12  10098  fin1a2lem13  10099  hsmexlem2  10114  axdc2lem  10135  imadomg  10221  fnct  10224  iundom2g  10227  iundomg  10228  iundom  10229  unirnfdomd  10254  konigthlem  10255  iunctb  10261  fpwwe2  10330  canthwelem  10337  pwfseqlem3  10347  pwfseqlem5  10350  winalim2  10383  wunelss  10395  r1wunlim  10424  wunex2  10425  tsksdom  10443  tskinf  10456  inttsk  10461  inar1  10462  tskcard  10468  tskurn  10476  gruina  10505  grur1a  10506  grur1  10507  addsrpr  10762  mulsrpr  10763  lemul12a  11763  lemulge11  11767  lediv12a  11798  fiminre2  11853  nngt0  11934  nn0ge2m1nn  12232  peano5uzi  12339  nn0ind-raph  12350  znnn0nn  12362  suprzub  12608  uzsupss  12609  rpge0  12672  fz0fzelfz0  13291  fz0fzdiffz0  13294  ige2m2fzo  13378  elfzodifsumelfzo  13381  elfzom1elp1fzo  13382  fzonfzoufzol  13418  flltdivnn0lt  13481  fldiv  13508  modaddmodup  13582  uzrdgsuci  13608  fzennn  13616  uzindi  13630  fsuppmapnn0fiubex  13640  expcl2lem  13722  leexp1a  13821  modexp  13881  faclbnd  13932  faclbnd6  13941  facavg  13943  hashginv  13976  hashf1rn  13995  hasheqf1od  13996  seqcoll  14106  hashge2el2dif  14122  wrdsymb0  14180  wrdlenge2n0  14183  ccatsymb  14215  swrdnd2  14296  swrdnd0  14298  pfxnd  14328  pfxccat1  14343  swrdpfx  14348  pfxpfx  14349  wrd2ind  14364  pfxccatin12  14374  pfxccat3  14375  swrdccat  14376  pfxccatpfx1  14377  pfxccatpfx2  14378  swrdccatin1d  14384  pfxccatin12d  14386  repswswrd  14425  cshwidxmod  14444  s2f1o  14557  f1oun2prg  14558  wwlktovfo  14601  relexpfld  14688  rtrclreclem3  14699  resqrex  14890  cau3lem  14994  reusq0  15102  rlimcld2  15215  climcn2  15230  isercoll  15307  climsup  15309  caurcvgr  15313  sumeq2ii  15333  summolem3  15354  zsum  15358  fsumadd  15380  fsumsplit1  15385  fsum2dlem  15410  fsum0diag2  15423  fsummulc2  15424  fsumabs  15441  fsumrelem  15447  fsumrlim  15451  fsumo1  15452  o1fsum  15453  fsumiun  15461  qshash  15467  prodeq2ii  15551  prodmolem3  15571  fprodmul  15598  fproddiv  15599  fprod2dlem  15618  fprodsplit1f  15628  sin02gt0  15829  efieq1re  15836  p1modz1  15898  dvdsleabs2  15949  4dvdseven  16010  sumeven  16024  sumodd  16025  divalglem9  16038  smupvallem  16118  algfx  16213  eucalgcvga  16219  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmflefac  16281  qredeq  16290  fermltl  16413  modprm0  16434  pythagtriplem4  16448  pythagtriplem6  16450  pythagtriplem7  16451  pythagtriplem12  16455  pythagtriplem13  16456  pythagtriplem14  16457  pythagtriplem16  16459  difsqpwdvds  16516  pcmpt  16521  prmreclem2  16546  4sqlem11  16584  vdwlem9  16618  vdwlem11  16620  vdwlem12  16621  0ram  16649  0ram2  16650  0ramcl  16652  ramcl  16658  prmolelcmf  16677  cshwsidrepsw  16723  cshwshashlem2  16726  prmlem1  16737  prmlem2  16749  strfvd  16830  strfv2d  16831  strssd  16835  firest  17060  prdsdsval3  17113  imasbas  17140  imasds  17141  imasaddfnlem  17156  imasaddvallem  17157  imasvscafn  17165  qusaddvallem  17179  qusaddflem  17180  qusaddval  17181  qusaddf  17182  qusmulval  17183  qusmulf  17184  catideu  17301  idinv  17418  brcici  17429  invfuc  17608  2initoinv  17641  initoeu1w  17643  initoeu2lem0  17644  2termoinv  17648  termoeu1w  17650  mod2ile  18127  lubss  18146  acsmapd  18187  lidrididd  18269  gsumval2a  18284  mndind  18381  submefmnd  18449  mgm2nsgrplem4  18475  qusgrp2  18608  mulgnegnn  18629  pgrpsubgsymg  18932  fvcosymgeq  18952  gsmsymgreqlem1  18953  psgnunilem4  19020  pgpssslw  19134  sylow2alem2  19138  fislw  19145  efgsres  19259  rinvmod  19325  gsumval3lem2  19422  gsumzaddlem  19437  gsum2d  19488  nn0gsumfz  19500  telgsums  19509  dprddomcld  19519  ablfac2  19607  srgi  19662  ringi  19714  qusring2  19774  lssintcl  20141  lbsextlem3  20337  lbsextlem4  20338  zringlpirlem3  20598  psgnodpm  20705  psgndiflemB  20717  frlmup4  20918  lindff1  20937  lindfrn  20938  lmisfree  20959  evlseu  21203  mhpmulcl  21249  mptcoe1fsupp  21296  cply1coe0bi  21381  mpfpf1  21427  pf1mpf  21428  mat0dimscm  21526  mdetdiagid  21657  mdet1  21658  mdetunilem9  21677  slesolinv  21737  cramerimp  21743  cpmatmcllem  21775  mptcoe1matfsupp  21859  mp2pm2mp  21868  chpdmat  21898  cctop  22064  subbascn  22313  cnss2  22336  cmpcovf  22450  2ndcctbss  22514  2ndcomap  22517  2ndcsep  22518  comppfsc  22591  ptclsg  22674  dfac14  22677  txcnp  22679  ptcnplem  22680  uptx  22684  txtube  22699  tx2ndc  22710  xkococnlem  22718  elqtop  22756  qtoprest  22776  indishmph  22857  ptcmpfi  22872  kqhmph  22878  csdfil  22953  filssufilg  22970  ufilen  22989  rnelfm  23012  fmfnfmlem4  23016  alexsubALTlem4  23109  ptcmplem4  23114  cnextfvval  23124  cnextcn  23126  cnextfres  23128  tmdgsum2  23155  imasf1oxmet  23436  metss  23570  met2ndci  23584  prdsxmslem2  23591  metust  23620  cfilucfil  23621  metustbl  23628  psmetutop  23629  opnreen  23900  rectbntr0  23901  fsumcn  23939  rescncf  23966  xrhmeo  24015  cnllycmp  24025  lebnumlem1  24030  lebnumlem3  24032  cfilss  24339  iscmet3lem1  24360  iscmet3lem2  24361  ivthicc  24527  ovolsslem  24553  ovoliunlem2  24572  ovoliunnul  24576  ovolicc2lem4  24589  voliunlem3  24621  volsup  24625  uniiccdif  24647  uniioombllem2  24652  volivth  24676  mbfimaopnlem  24724  mbflimsup  24735  i1fd  24750  itg1addlem4  24768  itg1addlem4OLD  24769  itg2addlem  24828  itg2gt0  24830  limciun  24963  dvadd  25009  dvmul  25010  dvco  25016  dvrec  25024  dvcnv  25046  dvferm  25057  rollelem  25058  dvlip  25062  dvlip2  25064  c1liplem1  25065  c1lip2  25067  dvgt0lem1  25071  dvivthlem1  25077  lhop1lem  25082  dvcnvrelem1  25086  dvcnvrelem2  25087  dvcvx  25089  dvfsumle  25090  dvfsumabs  25092  dvfsumlem1  25095  dvfsumlem2  25096  dvfsumlem4  25098  dvfsumrlim2  25101  dvfsum2  25103  ftc1cn  25112  ftc2ditglem  25114  itgsubstlem  25117  itgpowd  25119  tdeglem4OLD  25130  mdegaddle  25144  mdegmullem  25148  deg1sublt  25180  ply1divmo  25205  fta1g  25237  dgrub  25300  dgrnznn  25313  dgradd2  25334  dvply1  25349  plyrem  25370  aalioulem4  25400  aalioulem5  25401  aalioulem6  25402  aaliou2  25405  taylf  25425  ulmdv  25467  psercn2  25487  abelth  25505  abelth2  25506  reeff1olem  25510  efopn  25718  logreclem  25817  isosctrlem2  25874  xrlimcnp  26023  basellem4  26138  ppiwordi  26216  musum  26245  chpub  26273  gausslemma2dlem0c  26411  2sqlem6  26476  addsqnreup  26496  2sqreulem1  26499  2sqreunnlem1  26502  dchrisumlema  26541  dchrisumlem2  26543  dchrisumlem3  26544  pntlemp  26663  pntleml  26664  ostth3  26691  iscgrglt  26779  colline  26914  axlowdimlem16  27228  axlowdimlem17  27229  axcontlem3  27237  axcontlem10  27244  uhgr2edg  27478  nbupgruvtxres  27677  cusgrres  27718  cusgrfilem2  27726  vdumgr0  27750  frusgrnn0  27841  wlklenvclwlkOLD  27925  wlkp1lem8  27950  pthdivtx  27998  upgrwlkdvde  28006  spthonepeq  28021  usgr2pthlem  28032  lfgrn1cycl  28071  wwlknbp1  28110  wwlknllvtx  28112  wlkiswwlks2lem3  28137  umgr2adedgspth  28214  clwlkclwwlklem3  28266  clwwisshclwwslemlem  28278  clwwisshclwws  28280  clwwlkel  28311  wwlksubclwwlk  28323  eleclclwwlknlem1  28325  eleclclwwlknlem2  28326  erclwwlknref  28334  clwwlknonccat  28361  clwwlknonex2lem2  28373  3wlkdlem4  28427  vdn0conngrumgrv2  28461  eucrctshift  28508  frgrnbnb  28558  frgrncvvdeqlem2  28565  frgrncvvdeqlem3  28566  fusgreghash2wspv  28600  numclwwlk2lem1  28641  numclwlk2lem2f  28642  numclwwlk5  28653  numclwwlk7  28656  frgrreggt1  28658  minvecolem4b  29141  minvecolem4  29143  bcsiALT  29442  ococin  29671  spanpr  29843  pjorthi  29932  nmbdoplbi  30287  nmcoplbi  30291  nmbdfnlbi  30312  nmcfnlbi  30315  nmopcoi  30358  branmfn  30368  hstnmoc  30486  mdsl0  30573  atomli  30645  atcvat4i  30660  atabsi  30664  foresf1o  30751  rabfodom  30752  abrexdomjm  30753  elpreq  30779  ifeqeqx  30786  disjiunel  30836  fovcld  30876  aciunf1lem  30901  ffsrn  30966  xlt2addrd  30983  supxrnemnf  30993  ssnnssfz  31010  dvdszzq  31031  resspos  31146  resstos  31147  gsummptres2  31215  archirngz  31345  orngsqr  31405  isarchiofld  31418  elrspunidl  31508  prmidl2  31518  qsidomlem2  31531  ssmxidl  31544  locfinreflem  31692  cmpcref  31702  fmcncfil  31783  xrge0iifiso  31787  elzdif0  31830  qqhval2lem  31831  esumcst  31931  esumrnmpt2  31936  esumpinfval  31941  esumpinfsum  31945  sigaclci  32000  insiga  32005  ldgenpisys  32034  measres  32090  measdivcstALTV  32093  dya2iocnrect  32148  dya2iocnei  32149  omssubadd  32167  carsggect  32185  carsgclctunlem2  32186  sitgclg  32209  eulerpartlemsv2  32225  eulerpartlemv  32231  eulerpartlemf  32237  eulerpartlemgh  32245  eulerpartlemgs2  32247  ballotlemfp1  32358  ballotlemfrcn0  32396  ftc2re  32478  fdvposlt  32479  fdvposle  32481  bnj1379  32710  bnj580  32793  bnj944  32818  bnj999  32838  bnj1204  32892  bnj1398  32914  cusgredgex  32983  pthacycspth  33019  derangenlem  33033  subfacp1lem3  33044  resconn  33108  cvmliftlem3  33149  satfv0fvfmla0  33275  satfv1fvfmla1  33285  mrsub0  33378  ttrclss  33706  ttrclselem2  33712  naddssim  33764  sltres  33792  noextenddif  33798  nolesgn2ores  33802  nogesgn1ores  33804  nosep1o  33811  nosep2o  33812  nosepeq  33815  nolt02o  33825  noresle  33827  nosupno  33833  nosupbday  33835  nosupres  33837  nosupbnd1lem1  33838  nosupbnd1lem4  33841  nosupbnd1  33844  nosupbnd2lem1  33845  nosupbnd2  33846  noinfno  33848  noinfbday  33850  noinfres  33852  noinfbnd1lem5  33857  noinfbnd1  33859  noinfbnd2lem1  33860  madebday  34007  cgrextend  34237  segconeq  34239  trisegint  34257  fwddifnp1  34394  ivthALT  34451  fnessref  34473  refssfne  34474  neibastop1  34475  filnetlem4  34497  ontgval  34547  unblimceq0lem  34613  unbdqndv2lem2  34617  unbdqndv2  34618  bj-babygodel  34712  bj-alrimd  34728  bj-exlimd  34733  bj-spcimdv  35007  bj-spcimdvv  35008  bj-finsumval0  35383  bj-fvimacnv0  35384  dfgcd3  35422  relowlssretop  35461  relowlpssretop  35462  onsucuni3  35465  finxpreclem4  35492  poimirlem18  35722  poimirlem21  35725  poimirlem25  35729  ftc1cnnclem  35775  ftc1cnnc  35776  ftc2nc  35786  dvasin  35788  dvacos  35789  abrexdom  35815  indexdom  35819  mettrifi  35842  equivtotbnd  35863  totbndbnd  35874  prdstotbnd  35879  heibor1lem  35894  bfplem1  35907  bfplem2  35908  opidonOLD  35937  rngodm1dm2  36017  zerdivemp1x  36032  equid1  36840  omllaw5N  37188  cmtcomlemN  37189  cmtbr3N  37195  omlfh3N  37200  atlen0  37251  exatleN  37345  hlrelat3  37353  cvrexchlem  37360  atlelt  37379  cvrat4  37384  4atlem11b  37549  4atlem12b  37552  lneq2at  37719  cdlema1N  37732  cdlemblem  37734  paddss12  37760  paddasslem2  37762  paddasslem4  37764  paddasslem6  37766  paddasslem12  37772  paddunN  37868  poml4N  37894  poml5N  37895  osumcllem6N  37902  pexmidlem6N  37916  pl42lem2N  37921  ltrnu  38062  ltrneq2  38089  trlval2  38104  cdlemd6  38144  cdleme25b  38295  cdleme29b  38316  cdlemefr29exN  38343  ltrniotacnvval  38523  cdlemk28-3  38849  dochexmidlem7  39407  muldvds2d  39935  frlmsnic  40188  nna4b4nsq  40413  mzpsubmpt  40481  mzpsubst  40486  eqrabdioph  40515  rabdiophlem2  40540  elpell14qr2  40600  elpell1qr2  40610  pellfundre  40619  pellfundge  40620  pellfundglb  40623  pellfund14gap  40625  congabseq  40712  jm2.22  40733  jm2.23  40734  jm2.26lem3  40739  wepwsolem  40783  dnwech  40789  aomclem2  40796  aomclem4  40798  pwfi2f1o  40837  ss2iundf  41156  dssmapf1od  41518  neik0pk1imk0  41546  gneispace  41633  grur1cld  41739  cpcolld  41765  mnuop23d  41773  mnuprdlem1  41779  mnuprdlem2  41780  mnurndlem1  41788  grumnudlem  41792  radcnvrat  41821  sbiota1  41941  ordelordALT  42046  2pm13.193  42061  ee11an  42199  refsumcn  42462  rfcnnnub  42468  disjxp1  42506  xrnmnfpnf  42522  ssinc  42526  nssd  42544  disjf1o  42618  disjinfi  42620  choicefi  42629  axccdom  42651  dmrelrnrel  42654  monoords  42726  fperiodmullem  42732  xadd0ge  42749  xrssre  42777  xrlexaddrp  42781  xrred  42794  infxr  42796  xrnpnfmnf  42905  monoordxrv  42912  monoord2xrv  42914  fsumiunss  43006  fmul01  43011  fmuldfeqlem1  43013  fmuldfeq  43014  fmul01lt1lem1  43015  fmul01lt1lem2  43016  cncfmptss  43018  climinf  43037  climsuselem1  43038  climsuse  43039  limcperiod  43059  limcrecl  43060  sumnnodd  43061  limcleqr  43075  0ellimcdiv  43080  climleltrp  43107  limsuppnfdlem  43132  limsupresxr  43197  liminfresxr  43198  liminfvalxr  43214  cnrefiisplem  43260  xlimmnfvlem1  43263  xlimpnfvlem1  43267  cncfperiod  43310  icccncfext  43318  cncfiooicclem1  43324  dvbdfbdioolem1  43359  dvnmptdivc  43369  dvdsn1add  43370  dvnmptconst  43372  dvnmul  43374  dvmptfprodlem  43375  dvmptfprod  43376  dvnprodlem2  43378  iblspltprt  43404  itgsubsticclem  43406  itgspltprt  43410  itgsbtaddcnst  43413  stoweidlem3  43434  stoweidlem16  43447  stoweidlem17  43448  stoweidlem19  43450  stoweidlem20  43451  stoweidlem23  43454  stoweidlem25  43456  stoweidlem27  43458  stoweidlem31  43462  stoweidlem34  43465  stoweidlem42  43473  stoweidlem48  43479  stoweidlem51  43482  stoweidlem52  43483  stoweidlem59  43490  wallispilem1  43496  wallispilem3  43498  stirlinglem13  43517  fourierdlem16  43554  fourierdlem20  43558  fourierdlem21  43559  fourierdlem38  43576  fourierdlem42  43580  fourierdlem46  43583  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem54  43591  fourierdlem68  43605  fourierdlem72  43609  fourierdlem73  43610  fourierdlem76  43613  fourierdlem79  43616  fourierdlem81  43618  fourierdlem86  43623  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem92  43629  fourierdlem97  43634  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  etransclem24  43689  etransclem25  43690  etransclem28  43693  etransclem41  43706  etransclem44  43709  etransclem48  43713  salexct  43763  dfsalgen2  43770  sge0f1o  43810  sge0rnbnd  43821  sge0split  43837  sge0iunmptlemre  43843  sge0fodjrnlem  43844  sge0iunmpt  43846  nnfoctbdjlem  43883  iundjiunlem  43887  meadjiunlem  43893  ismeannd  43895  meaiuninclem  43908  omeiunle  43945  carageniuncllem1  43949  caratheodorylem1  43954  hoidmvlelem4  44026  hoiqssbllem2  44051  salpreimagelt  44132  salpreimalegt  44134  pimdecfgtioc  44139  smfaddlem2  44186  smflimlem6  44198  nsssmfmbflem  44200  smfpimcclem  44227  or2expropbilem1  44413  funressndmfvrn  44425  f1cof1b  44456  2leaddle2  44678  smonoord  44711  uniimaprimaeqfv  44722  fundcmpsurbijinjpreimafv  44747  fundcmpsurinjALT  44752  iccpartf  44771  ich2exprop  44811  ichnreuop  44812  ichreuopeq  44813  sprbisymrel  44839  fmtnodvds  44884  proththdlem  44953  gbowgt5  45102  gboge9  45104  gbege6  45105  stgoldbwt  45116  sbgoldbalt  45121  bgoldbnnsum3prm  45144  isomgrtrlem  45178  uspgrbisymrelALT  45205  ssnn0ssfz  45573  ldepspr  45702  seposep  46107  subthinc  46209  prsthinc  46223  iunord  46268  bnd2d  46273  setrecsss  46292