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  512  syl2anc  584  unitreslOLD  875  aevlem0  2058  equvel  2457  ralimda  3432  elex2OLD  3454  elex22  3455  spcedv  3538  rspcdf  3549  rspcdva  3563  spsbcd  3731  opth  5392  euotd  5428  wereu2  5587  unielrel  6181  frpomin  6247  tz7.7  6296  funmo  6456  funmoOLD  6457  fvelimad  6845  iinpreima  6955  fnfvima  7118  resfvresima  7120  fliftfun  7192  fliftval  7196  weniso  7234  riota5f  7270  riotass2  7272  ofmpteq  7564  ssorduni  7638  sucexeloni  7667  suceloniOLD  7669  nlimsucg  7698  tfisi  7714  zfrep6  7806  curry1  7953  curry2  7956  fnwelem  7981  funsssuppss  8015  frrlem4  8114  frrlem8  8118  frrlem10  8120  fprlem1  8125  fprlem2  8126  wfrlem4OLD  8152  smogt  8207  tfrlem5  8220  omeulem1  8422  oeworde  8433  oelimcl  8440  oeeulem  8441  oeeui  8442  nnawordex  8477  oaabs2  8488  swoso  8540  qliftlem  8596  resixp  8730  undomOLD  8856  xpdom3  8866  domunsncan  8868  omxpenlem  8869  domssex  8934  xpf1o  8935  mapdom3  8945  findcard  8955  f1dmvrnfibi  9112  fiin  9190  marypha1lem  9201  marypha1  9202  fisupcl  9237  supgtoreq  9238  ordiso2  9283  ordtypelem2  9287  ordtypelem8  9293  wemapso2lem  9320  unxpwdom2  9356  cantnflt  9439  cantnfrescl  9443  oemapvali  9451  cantnflem1d  9455  wemapwe  9464  cnfcom  9467  ttrclss  9487  ttrclselem2  9493  frrlem15  9524  rankr1id  9629  tcrank  9651  cardmin2  9766  infxpenlem  9778  fseqen  9792  ween  9800  ac5num  9801  indcardi  9806  acni2  9811  fodomfi2  9825  infpwfien  9827  inffien  9828  iunfictbso  9879  acacni  9905  dfac12lem2  9909  djuinf  9953  infmap2  9983  ackbij1lem18  10002  ackbij1b  10004  fictb  10010  cfslb2n  10033  cofsmo  10034  cfsmolem  10035  coftr  10038  infpssrlem4  10071  domfin4  10076  fin2i2  10083  isfin2-2  10084  fincssdom  10088  ssfin3ds  10095  fin23lem20  10102  fin23lem30  10107  isf32lem3  10120  fin1a2lem12  10176  fin1a2lem13  10177  hsmexlem2  10192  axdc2lem  10213  imadomg  10299  fnct  10302  iundom2g  10305  iundomg  10306  iundom  10307  unirnfdomd  10332  konigthlem  10333  iunctb  10339  fpwwe2  10408  canthwelem  10415  pwfseqlem3  10425  pwfseqlem5  10428  winalim2  10461  wunelss  10473  r1wunlim  10502  wunex2  10503  tsksdom  10521  tskinf  10534  inttsk  10539  inar1  10540  tskcard  10546  tskurn  10554  gruina  10583  grur1a  10584  grur1  10585  addsrpr  10840  mulsrpr  10841  lemul12a  11842  lemulge11  11846  lediv12a  11877  fiminre2  11932  nngt0  12013  nn0ge2m1nn  12311  peano5uzi  12418  nn0ind-raph  12429  znnn0nn  12442  suprzub  12688  uzsupss  12689  rpge0  12752  fz0fzelfz0  13371  fz0fzdiffz0  13374  ige2m2fzo  13459  elfzodifsumelfzo  13462  elfzom1elp1fzo  13463  fzonfzoufzol  13499  flltdivnn0lt  13562  fldiv  13589  modaddmodup  13663  uzrdgsuci  13689  fzennn  13697  uzindi  13711  fsuppmapnn0fiubex  13721  expcl2lem  13803  leexp1a  13902  modexp  13962  faclbnd  14013  faclbnd6  14022  facavg  14024  hashginv  14057  hashf1rn  14076  hasheqf1od  14077  seqcoll  14187  hashge2el2dif  14203  wrdsymb0  14261  wrdlenge2n0  14264  ccatsymb  14296  swrdnd2  14377  swrdnd0  14379  pfxnd  14409  pfxccat1  14424  swrdpfx  14429  pfxpfx  14430  wrd2ind  14445  pfxccatin12  14455  pfxccat3  14456  swrdccat  14457  pfxccatpfx1  14458  pfxccatpfx2  14459  swrdccatin1d  14465  pfxccatin12d  14467  repswswrd  14506  cshwidxmod  14525  s2f1o  14638  f1oun2prg  14639  wwlktovfo  14682  relexpfld  14769  rtrclreclem3  14780  resqrex  14971  cau3lem  15075  reusq0  15183  rlimcld2  15296  climcn2  15311  isercoll  15388  climsup  15390  caurcvgr  15394  sumeq2ii  15414  summolem3  15435  zsum  15439  fsumadd  15461  fsumsplit1  15466  fsum2dlem  15491  fsum0diag2  15504  fsummulc2  15505  fsumabs  15522  fsumrelem  15528  fsumrlim  15532  fsumo1  15533  o1fsum  15534  fsumiun  15542  qshash  15548  prodeq2ii  15632  prodmolem3  15652  fprodmul  15679  fproddiv  15680  fprod2dlem  15699  fprodsplit1f  15709  sin02gt0  15910  efieq1re  15917  p1modz1  15979  dvdsleabs2  16030  4dvdseven  16091  sumeven  16105  sumodd  16106  divalglem9  16119  smupvallem  16199  algfx  16294  eucalgcvga  16300  lcmfunsnlem1  16351  lcmfunsnlem2lem1  16352  lcmflefac  16362  qredeq  16371  fermltl  16494  modprm0  16515  pythagtriplem4  16529  pythagtriplem6  16531  pythagtriplem7  16532  pythagtriplem12  16536  pythagtriplem13  16537  pythagtriplem14  16538  pythagtriplem16  16540  difsqpwdvds  16597  pcmpt  16602  prmreclem2  16627  4sqlem11  16665  vdwlem9  16699  vdwlem11  16701  vdwlem12  16702  0ram  16730  0ram2  16731  0ramcl  16733  ramcl  16739  prmolelcmf  16758  cshwsidrepsw  16804  cshwshashlem2  16807  prmlem1  16818  prmlem2  16830  strfvd  16911  strfv2d  16912  strssd  16916  firest  17152  prdsdsval3  17205  imasbas  17232  imasds  17233  imasaddfnlem  17248  imasaddvallem  17249  imasvscafn  17257  qusaddvallem  17271  qusaddflem  17272  qusaddval  17273  qusaddf  17274  qusmulval  17275  qusmulf  17276  catideu  17393  idinv  17510  brcici  17521  invfuc  17701  2initoinv  17734  initoeu1w  17736  initoeu2lem0  17737  2termoinv  17741  termoeu1w  17743  mod2ile  18221  lubss  18240  acsmapd  18281  lidrididd  18363  gsumval2a  18378  mndind  18475  submefmnd  18543  mgm2nsgrplem4  18569  qusgrp2  18702  mulgnegnn  18723  pgrpsubgsymg  19026  fvcosymgeq  19046  gsmsymgreqlem1  19047  psgnunilem4  19114  pgpssslw  19228  sylow2alem2  19232  fislw  19239  efgsres  19353  rinvmod  19419  gsumval3lem2  19516  gsumzaddlem  19531  gsum2d  19582  nn0gsumfz  19594  telgsums  19603  dprddomcld  19613  ablfac2  19701  srgi  19756  ringi  19808  qusring2  19868  lssintcl  20235  lbsextlem3  20431  lbsextlem4  20432  zringlpirlem3  20695  psgnodpm  20802  psgndiflemB  20814  frlmup4  21017  lindff1  21036  lindfrn  21037  lmisfree  21058  evlseu  21302  mhpmulcl  21348  mptcoe1fsupp  21395  cply1coe0bi  21480  mpfpf1  21526  pf1mpf  21527  mat0dimscm  21627  mdetdiagid  21758  mdet1  21759  mdetunilem9  21778  slesolinv  21838  cramerimp  21844  cpmatmcllem  21876  mptcoe1matfsupp  21960  mp2pm2mp  21969  chpdmat  21999  cctop  22165  subbascn  22414  cnss2  22437  cmpcovf  22551  2ndcctbss  22615  2ndcomap  22618  2ndcsep  22619  comppfsc  22692  ptclsg  22775  dfac14  22778  txcnp  22780  ptcnplem  22781  uptx  22785  txtube  22800  tx2ndc  22811  xkococnlem  22819  elqtop  22857  qtoprest  22877  indishmph  22958  ptcmpfi  22973  kqhmph  22979  csdfil  23054  filssufilg  23071  ufilen  23090  rnelfm  23113  fmfnfmlem4  23117  alexsubALTlem4  23210  ptcmplem4  23215  cnextfvval  23225  cnextcn  23227  cnextfres  23229  tmdgsum2  23256  imasf1oxmet  23537  metss  23673  met2ndci  23687  prdsxmslem2  23694  metust  23723  cfilucfil  23724  metustbl  23731  psmetutop  23732  opnreen  24003  rectbntr0  24004  fsumcn  24042  rescncf  24069  xrhmeo  24118  cnllycmp  24128  lebnumlem1  24133  lebnumlem3  24135  cfilss  24443  iscmet3lem1  24464  iscmet3lem2  24465  ivthicc  24631  ovolsslem  24657  ovoliunlem2  24676  ovoliunnul  24680  ovolicc2lem4  24693  voliunlem3  24725  volsup  24729  uniiccdif  24751  uniioombllem2  24756  volivth  24780  mbfimaopnlem  24828  mbflimsup  24839  i1fd  24854  itg1addlem4  24872  itg1addlem4OLD  24873  itg2addlem  24932  itg2gt0  24934  limciun  25067  dvadd  25113  dvmul  25114  dvco  25120  dvrec  25128  dvcnv  25150  dvferm  25161  rollelem  25162  dvlip  25166  dvlip2  25168  c1liplem1  25169  c1lip2  25171  dvgt0lem1  25175  dvivthlem1  25181  lhop1lem  25186  dvcnvrelem1  25190  dvcnvrelem2  25191  dvcvx  25193  dvfsumle  25194  dvfsumabs  25196  dvfsumlem1  25199  dvfsumlem2  25200  dvfsumlem4  25202  dvfsumrlim2  25205  dvfsum2  25207  ftc1cn  25216  ftc2ditglem  25218  itgsubstlem  25221  itgpowd  25223  tdeglem4OLD  25234  mdegaddle  25248  mdegmullem  25252  deg1sublt  25284  ply1divmo  25309  fta1g  25341  dgrub  25404  dgrnznn  25417  dgradd2  25438  dvply1  25453  plyrem  25474  aalioulem4  25504  aalioulem5  25505  aalioulem6  25506  aaliou2  25509  taylf  25529  ulmdv  25571  psercn2  25591  abelth  25609  abelth2  25610  reeff1olem  25614  efopn  25822  logreclem  25921  isosctrlem2  25978  xrlimcnp  26127  basellem4  26242  ppiwordi  26320  musum  26349  chpub  26377  gausslemma2dlem0c  26515  2sqlem6  26580  addsqnreup  26600  2sqreulem1  26603  2sqreunnlem1  26606  dchrisumlema  26645  dchrisumlem2  26647  dchrisumlem3  26648  pntlemp  26767  pntleml  26768  ostth3  26795  iscgrglt  26884  colline  27019  axlowdimlem16  27334  axlowdimlem17  27335  axcontlem3  27343  axcontlem10  27350  uhgr2edg  27584  nbupgruvtxres  27783  cusgrres  27824  cusgrfilem2  27832  vdumgr0  27856  frusgrnn0  27947  wlklenvclwlkOLD  28032  wlkp1lem8  28057  pthdivtx  28106  upgrwlkdvde  28114  spthonepeq  28129  usgr2pthlem  28140  lfgrn1cycl  28179  wwlknbp1  28218  wwlknllvtx  28220  wlkiswwlks2lem3  28245  umgr2adedgspth  28322  clwlkclwwlklem3  28374  clwwisshclwwslemlem  28386  clwwisshclwws  28388  clwwlkel  28419  wwlksubclwwlk  28431  eleclclwwlknlem1  28433  eleclclwwlknlem2  28434  erclwwlknref  28442  clwwlknonccat  28469  clwwlknonex2lem2  28481  3wlkdlem4  28535  vdn0conngrumgrv2  28569  eucrctshift  28616  frgrnbnb  28666  frgrncvvdeqlem2  28673  frgrncvvdeqlem3  28674  fusgreghash2wspv  28708  numclwwlk2lem1  28749  numclwlk2lem2f  28750  numclwwlk5  28761  numclwwlk7  28764  frgrreggt1  28766  minvecolem4b  29249  minvecolem4  29251  bcsiALT  29550  ococin  29779  spanpr  29951  pjorthi  30040  nmbdoplbi  30395  nmcoplbi  30399  nmbdfnlbi  30420  nmcfnlbi  30423  nmopcoi  30466  branmfn  30476  hstnmoc  30594  mdsl0  30681  atomli  30753  atcvat4i  30768  atabsi  30772  foresf1o  30859  rabfodom  30860  abrexdomjm  30861  elpreq  30887  ifeqeqx  30894  disjiunel  30944  fovcld  30984  aciunf1lem  31008  ffsrn  31073  xlt2addrd  31090  supxrnemnf  31100  ssnnssfz  31117  dvdszzq  31138  resspos  31253  resstos  31254  gsummptres2  31322  archirngz  31452  orngsqr  31512  isarchiofld  31525  elrspunidl  31615  prmidl2  31625  qsidomlem2  31638  ssmxidl  31651  locfinreflem  31799  cmpcref  31809  fmcncfil  31890  xrge0iifiso  31894  elzdif0  31939  qqhval2lem  31940  esumcst  32040  esumrnmpt2  32045  esumpinfval  32050  esumpinfsum  32054  sigaclci  32109  insiga  32114  ldgenpisys  32143  measres  32199  measdivcstALTV  32202  dya2iocnrect  32257  dya2iocnei  32258  omssubadd  32276  carsggect  32294  carsgclctunlem2  32295  sitgclg  32318  eulerpartlemsv2  32334  eulerpartlemv  32340  eulerpartlemf  32346  eulerpartlemgh  32354  eulerpartlemgs2  32356  ballotlemfp1  32467  ballotlemfrcn0  32505  ftc2re  32587  fdvposlt  32588  fdvposle  32590  bnj1379  32819  bnj580  32902  bnj944  32927  bnj999  32947  bnj1204  33001  bnj1398  33023  cusgredgex  33092  pthacycspth  33128  derangenlem  33142  subfacp1lem3  33153  resconn  33217  cvmliftlem3  33258  satfv0fvfmla0  33384  satfv1fvfmla1  33394  mrsub0  33487  naddssim  33846  sltres  33874  noextenddif  33880  nolesgn2ores  33884  nogesgn1ores  33886  nosep1o  33893  nosep2o  33894  nosepeq  33897  nolt02o  33907  noresle  33909  nosupno  33915  nosupbday  33917  nosupres  33919  nosupbnd1lem1  33920  nosupbnd1lem4  33923  nosupbnd1  33926  nosupbnd2lem1  33927  nosupbnd2  33928  noinfno  33930  noinfbday  33932  noinfres  33934  noinfbnd1lem5  33939  noinfbnd1  33941  noinfbnd2lem1  33942  madebday  34089  cgrextend  34319  segconeq  34321  trisegint  34339  fwddifnp1  34476  ivthALT  34533  fnessref  34555  refssfne  34556  neibastop1  34557  filnetlem4  34579  ontgval  34629  unblimceq0lem  34695  unbdqndv2lem2  34699  unbdqndv2  34700  bj-babygodel  34794  bj-alrimd  34810  bj-exlimd  34815  bj-spcimdv  35089  bj-spcimdvv  35090  bj-finsumval0  35465  bj-fvimacnv0  35466  dfgcd3  35504  relowlssretop  35543  relowlpssretop  35544  onsucuni3  35547  finxpreclem4  35574  poimirlem18  35804  poimirlem21  35807  poimirlem25  35811  ftc1cnnclem  35857  ftc1cnnc  35858  ftc2nc  35868  dvasin  35870  dvacos  35871  abrexdom  35897  indexdom  35901  mettrifi  35924  equivtotbnd  35945  totbndbnd  35956  prdstotbnd  35961  heibor1lem  35976  bfplem1  35989  bfplem2  35990  opidonOLD  36019  rngodm1dm2  36099  zerdivemp1x  36114  equid1  36920  omllaw5N  37268  cmtcomlemN  37269  cmtbr3N  37275  omlfh3N  37280  atlen0  37331  exatleN  37425  hlrelat3  37433  cvrexchlem  37440  atlelt  37459  cvrat4  37464  4atlem11b  37629  4atlem12b  37632  lneq2at  37799  cdlema1N  37812  cdlemblem  37814  paddss12  37840  paddasslem2  37842  paddasslem4  37844  paddasslem6  37846  paddasslem12  37852  paddunN  37948  poml4N  37974  poml5N  37975  osumcllem6N  37982  pexmidlem6N  37996  pl42lem2N  38001  ltrnu  38142  ltrneq2  38169  trlval2  38184  cdlemd6  38224  cdleme25b  38375  cdleme29b  38396  cdlemefr29exN  38423  ltrniotacnvval  38603  cdlemk28-3  38929  dochexmidlem7  39487  muldvds2d  40014  frlmsnic  40270  nna4b4nsq  40504  mzpsubmpt  40572  mzpsubst  40577  eqrabdioph  40606  rabdiophlem2  40631  elpell14qr2  40691  elpell1qr2  40701  pellfundre  40710  pellfundge  40711  pellfundglb  40714  pellfund14gap  40716  congabseq  40803  jm2.22  40824  jm2.23  40825  jm2.26lem3  40830  wepwsolem  40874  dnwech  40880  aomclem2  40887  aomclem4  40889  pwfi2f1o  40928  ss2iundf  41274  dssmapf1od  41636  neik0pk1imk0  41664  gneispace  41751  grur1cld  41857  cpcolld  41883  mnuop23d  41891  mnuprdlem1  41897  mnuprdlem2  41898  mnurndlem1  41906  grumnudlem  41910  radcnvrat  41939  sbiota1  42059  ordelordALT  42164  2pm13.193  42179  ee11an  42317  refsumcn  42580  rfcnnnub  42586  disjxp1  42624  xrnmnfpnf  42640  ssinc  42644  nssd  42662  disjf1o  42736  disjinfi  42738  choicefi  42747  axccdom  42769  dmrelrnrel  42772  monoords  42843  fperiodmullem  42849  xadd0ge  42866  xrssre  42894  xrlexaddrp  42898  xrred  42911  infxr  42913  xrnpnfmnf  43022  monoordxrv  43029  monoord2xrv  43031  fsumiunss  43123  fmul01  43128  fmuldfeqlem1  43130  fmuldfeq  43131  fmul01lt1lem1  43132  fmul01lt1lem2  43133  cncfmptss  43135  climinf  43154  climsuselem1  43155  climsuse  43156  limcperiod  43176  limcrecl  43177  sumnnodd  43178  limcleqr  43192  0ellimcdiv  43197  climleltrp  43224  limsuppnfdlem  43249  limsupresxr  43314  liminfresxr  43315  liminfvalxr  43331  cnrefiisplem  43377  xlimmnfvlem1  43380  xlimpnfvlem1  43384  cncfperiod  43427  icccncfext  43435  cncfiooicclem1  43441  dvbdfbdioolem1  43476  dvnmptdivc  43486  dvdsn1add  43487  dvnmptconst  43489  dvnmul  43491  dvmptfprodlem  43492  dvmptfprod  43493  dvnprodlem2  43495  iblspltprt  43521  itgsubsticclem  43523  itgspltprt  43527  itgsbtaddcnst  43530  stoweidlem3  43551  stoweidlem16  43564  stoweidlem17  43565  stoweidlem19  43567  stoweidlem20  43568  stoweidlem23  43571  stoweidlem25  43573  stoweidlem27  43575  stoweidlem31  43579  stoweidlem34  43582  stoweidlem42  43590  stoweidlem48  43596  stoweidlem51  43599  stoweidlem52  43600  stoweidlem59  43607  wallispilem1  43613  wallispilem3  43615  stirlinglem13  43634  fourierdlem16  43671  fourierdlem20  43675  fourierdlem21  43676  fourierdlem38  43693  fourierdlem42  43697  fourierdlem46  43700  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem54  43708  fourierdlem68  43722  fourierdlem72  43726  fourierdlem73  43727  fourierdlem76  43730  fourierdlem79  43733  fourierdlem81  43735  fourierdlem86  43740  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem92  43746  fourierdlem97  43751  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  etransclem24  43806  etransclem25  43807  etransclem28  43810  etransclem41  43823  etransclem44  43826  etransclem48  43830  salexct  43880  dfsalgen2  43887  sge0f1o  43927  sge0rnbnd  43938  sge0split  43954  sge0iunmptlemre  43960  sge0fodjrnlem  43961  sge0iunmpt  43963  nnfoctbdjlem  44000  iundjiunlem  44004  meadjiunlem  44010  ismeannd  44012  meaiuninclem  44025  omeiunle  44062  carageniuncllem1  44066  caratheodorylem1  44071  hoidmvlelem4  44143  hoiqssbllem2  44168  salpreimagelt  44252  salpreimalegt  44254  pimdecfgtioc  44260  smfaddlem2  44309  smflimlem6  44321  nsssmfmbflem  44323  smfpimcclem  44351  or2expropbilem1  44537  funressndmfvrn  44549  f1cof1b  44580  2leaddle2  44801  smonoord  44834  uniimaprimaeqfv  44845  fundcmpsurbijinjpreimafv  44870  fundcmpsurinjALT  44875  iccpartf  44894  ich2exprop  44934  ichnreuop  44935  ichreuopeq  44936  sprbisymrel  44962  fmtnodvds  45007  proththdlem  45076  gbowgt5  45225  gboge9  45227  gbege6  45228  stgoldbwt  45239  sbgoldbalt  45244  bgoldbnnsum3prm  45267  isomgrtrlem  45301  uspgrbisymrelALT  45328  ssnn0ssfz  45696  ldepspr  45825  seposep  46230  subthinc  46332  prsthinc  46346  iunord  46393  bnd2d  46398  setrecsss  46417