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  jcnd  166  2thd  268  jca  515  syl2anc  587  unitreslOLD  878  aevlem0  2062  equvel  2455  ralimda  3397  elex2  3419  elex22  3420  spcedv  3503  rspcdf  3514  rspcdva  3529  spsbcd  3697  opth  5345  euotd  5381  wereu2  5533  unielrel  6117  frpomin  6172  tz7.7  6217  funmo  6374  fvelimad  6757  iinpreima  6867  fnfvima  7027  resfvresima  7029  fliftfun  7099  fliftval  7103  weniso  7141  riota5f  7177  riotass2  7179  ofmpteq  7468  ssorduni  7541  suceloni  7570  nlimsucg  7599  tfisi  7615  zfrep6  7706  curry1  7850  curry2  7853  fnwelem  7876  funsssuppss  7910  frrlem4  8008  frrlem8  8012  frrlem10  8014  fprlem1  8019  fprlem2  8020  wfrlem4  8036  smogt  8082  tfrlem5  8094  omeulem1  8288  oeworde  8299  oelimcl  8306  oeeulem  8307  oeeui  8308  nnawordex  8343  oaabs2  8352  swoso  8402  qliftlem  8458  resixp  8592  undom  8711  xpdom3  8721  domunsncan  8723  omxpenlem  8724  domssex  8785  xpf1o  8786  mapdom3  8796  findcard  8819  f1dmvrnfibi  8938  fiin  9016  marypha1lem  9027  marypha1  9028  fisupcl  9063  supgtoreq  9064  ordiso2  9109  ordtypelem2  9113  ordtypelem8  9119  wemapso2lem  9146  unxpwdom2  9182  cantnflt  9265  cantnfrescl  9269  oemapvali  9277  cantnflem1d  9281  wemapwe  9290  cnfcom  9293  rankr1id  9443  tcrank  9465  cardmin2  9580  infxpenlem  9592  fseqen  9606  ween  9614  ac5num  9615  indcardi  9620  acni2  9625  fodomfi2  9639  infpwfien  9641  inffien  9642  iunfictbso  9693  acacni  9719  dfac12lem2  9723  djuinf  9767  infmap2  9797  ackbij1lem18  9816  ackbij1b  9818  fictb  9824  cfslb2n  9847  cofsmo  9848  cfsmolem  9849  coftr  9852  infpssrlem4  9885  domfin4  9890  fin2i2  9897  isfin2-2  9898  fincssdom  9902  ssfin3ds  9909  fin23lem20  9916  fin23lem30  9921  isf32lem3  9934  fin1a2lem12  9990  fin1a2lem13  9991  hsmexlem2  10006  axdc2lem  10027  imadomg  10113  fnct  10116  iundom2g  10119  iundomg  10120  iundom  10121  unirnfdomd  10146  konigthlem  10147  iunctb  10153  fpwwe2  10222  canthwelem  10229  pwfseqlem3  10239  pwfseqlem5  10242  winalim2  10275  wunelss  10287  r1wunlim  10316  wunex2  10317  tsksdom  10335  tskinf  10348  inttsk  10353  inar1  10354  tskcard  10360  tskurn  10368  gruina  10397  grur1a  10398  grur1  10399  addsrpr  10654  mulsrpr  10655  lemul12a  11655  lemulge11  11659  lediv12a  11690  fiminre2  11745  nngt0  11826  nn0ge2m1nn  12124  peano5uzi  12231  nn0ind-raph  12242  znnn0nn  12254  suprzub  12500  uzsupss  12501  rpge0  12564  fz0fzelfz0  13183  fz0fzdiffz0  13186  ige2m2fzo  13270  elfzodifsumelfzo  13273  elfzom1elp1fzo  13274  fzonfzoufzol  13310  flltdivnn0lt  13373  fldiv  13398  modaddmodup  13472  uzrdgsuci  13498  fzennn  13506  uzindi  13520  fsuppmapnn0fiubex  13530  expcl2lem  13612  leexp1a  13710  modexp  13770  faclbnd  13821  faclbnd6  13830  facavg  13832  hashginv  13865  hashf1rn  13884  hasheqf1od  13885  seqcoll  13995  hashge2el2dif  14011  wrdsymb0  14069  wrdlenge2n0  14072  ccatsymb  14104  swrdnd2  14185  swrdnd0  14187  pfxnd  14217  pfxccat1  14232  swrdpfx  14237  pfxpfx  14238  wrd2ind  14253  pfxccatin12  14263  pfxccat3  14264  swrdccat  14265  pfxccatpfx1  14266  pfxccatpfx2  14267  swrdccatin1d  14273  pfxccatin12d  14275  repswswrd  14314  cshwidxmod  14333  s2f1o  14446  f1oun2prg  14447  wwlktovfo  14490  relexpfld  14577  rtrclreclem3  14588  resqrex  14779  cau3lem  14883  reusq0  14991  rlimcld2  15104  climcn2  15119  isercoll  15196  climsup  15198  caurcvgr  15202  sumeq2ii  15222  summolem3  15243  zsum  15247  fsumadd  15268  fsum2dlem  15297  fsum0diag2  15310  fsummulc2  15311  fsumabs  15328  fsumrelem  15334  fsumrlim  15338  fsumo1  15339  o1fsum  15340  fsumiun  15348  qshash  15354  prodeq2ii  15438  prodmolem3  15458  fprodmul  15485  fproddiv  15486  fprod2dlem  15505  fprodsplit1f  15515  sin02gt0  15716  efieq1re  15723  p1modz1  15785  dvdsleabs2  15836  4dvdseven  15897  sumeven  15911  sumodd  15912  divalglem9  15925  smupvallem  16005  algfx  16100  eucalgcvga  16106  lcmfunsnlem1  16157  lcmfunsnlem2lem1  16158  lcmflefac  16168  qredeq  16177  fermltl  16300  modprm0  16321  pythagtriplem4  16335  pythagtriplem6  16337  pythagtriplem7  16338  pythagtriplem12  16342  pythagtriplem13  16343  pythagtriplem14  16344  pythagtriplem16  16346  difsqpwdvds  16403  pcmpt  16408  prmreclem2  16433  4sqlem11  16471  vdwlem9  16505  vdwlem11  16507  vdwlem12  16508  0ram  16536  0ram2  16537  0ramcl  16539  ramcl  16545  prmolelcmf  16564  cshwsidrepsw  16610  cshwshashlem2  16613  prmlem1  16624  prmlem2  16636  strfvd  16710  strfv2d  16711  strssd  16715  firest  16891  prdsdsval3  16944  imasbas  16971  imasds  16972  imasaddfnlem  16987  imasaddvallem  16988  imasvscafn  16996  qusaddvallem  17010  qusaddflem  17011  qusaddval  17012  qusaddf  17013  qusmulval  17014  qusmulf  17015  catideu  17132  idinv  17248  brcici  17259  invfuc  17437  2initoinv  17470  initoeu1w  17472  initoeu2lem0  17473  2termoinv  17477  termoeu1w  17479  mod2ile  17954  lubss  17973  acsmapd  18014  lidrididd  18096  gsumval2a  18111  mndind  18208  submefmnd  18276  mgm2nsgrplem4  18302  qusgrp2  18435  mulgnegnn  18456  pgrpsubgsymg  18755  fvcosymgeq  18775  gsmsymgreqlem1  18776  psgnunilem4  18843  pgpssslw  18957  sylow2alem2  18961  fislw  18968  efgsres  19082  rinvmod  19148  gsumval3lem2  19245  gsumzaddlem  19260  gsum2d  19311  nn0gsumfz  19323  telgsums  19332  dprddomcld  19342  ablfac2  19430  srgi  19480  ringi  19532  qusring2  19592  lssintcl  19955  lbsextlem3  20151  lbsextlem4  20152  zringlpirlem3  20405  psgnodpm  20504  psgndiflemB  20516  frlmup4  20717  lindff1  20736  lindfrn  20737  lmisfree  20758  evlseu  20997  mhpmulcl  21043  mptcoe1fsupp  21090  cply1coe0bi  21175  mpfpf1  21221  pf1mpf  21222  mat0dimscm  21320  mdetdiagid  21451  mdet1  21452  mdetunilem9  21471  slesolinv  21531  cramerimp  21537  cpmatmcllem  21569  mptcoe1matfsupp  21653  mp2pm2mp  21662  chpdmat  21692  cctop  21857  subbascn  22105  cnss2  22128  cmpcovf  22242  2ndcctbss  22306  2ndcomap  22309  2ndcsep  22310  comppfsc  22383  ptclsg  22466  dfac14  22469  txcnp  22471  ptcnplem  22472  uptx  22476  txtube  22491  tx2ndc  22502  xkococnlem  22510  elqtop  22548  qtoprest  22568  indishmph  22649  ptcmpfi  22664  kqhmph  22670  csdfil  22745  filssufilg  22762  ufilen  22781  rnelfm  22804  fmfnfmlem4  22808  alexsubALTlem4  22901  ptcmplem4  22906  cnextfvval  22916  cnextcn  22918  cnextfres  22920  tmdgsum2  22947  imasf1oxmet  23227  metss  23360  met2ndci  23374  prdsxmslem2  23381  metust  23410  cfilucfil  23411  metustbl  23418  psmetutop  23419  opnreen  23682  rectbntr0  23683  fsumcn  23721  rescncf  23748  xrhmeo  23797  cnllycmp  23807  lebnumlem1  23812  lebnumlem3  23814  cfilss  24121  iscmet3lem1  24142  iscmet3lem2  24143  ivthicc  24309  ovolsslem  24335  ovoliunlem2  24354  ovoliunnul  24358  ovolicc2lem4  24371  voliunlem3  24403  volsup  24407  uniiccdif  24429  uniioombllem2  24434  volivth  24458  mbfimaopnlem  24506  mbflimsup  24517  i1fd  24532  itg1addlem4  24550  itg1addlem4OLD  24551  itg2addlem  24610  itg2gt0  24612  limciun  24745  dvadd  24791  dvmul  24792  dvco  24798  dvrec  24806  dvcnv  24828  dvferm  24839  rollelem  24840  dvlip  24844  dvlip2  24846  c1liplem1  24847  c1lip2  24849  dvgt0lem1  24853  dvivthlem1  24859  lhop1lem  24864  dvcnvrelem1  24868  dvcnvrelem2  24869  dvcvx  24871  dvfsumle  24872  dvfsumabs  24874  dvfsumlem1  24877  dvfsumlem2  24878  dvfsumlem4  24880  dvfsumrlim2  24883  dvfsum2  24885  ftc1cn  24894  ftc2ditglem  24896  itgsubstlem  24899  itgpowd  24901  tdeglem4OLD  24912  mdegaddle  24926  mdegmullem  24930  deg1sublt  24962  ply1divmo  24987  fta1g  25019  dgrub  25082  dgrnznn  25095  dgradd2  25116  dvply1  25131  plyrem  25152  aalioulem4  25182  aalioulem5  25183  aalioulem6  25184  aaliou2  25187  taylf  25207  ulmdv  25249  psercn2  25269  abelth  25287  abelth2  25288  reeff1olem  25292  efopn  25500  logreclem  25599  isosctrlem2  25656  xrlimcnp  25805  basellem4  25920  ppiwordi  25998  musum  26027  chpub  26055  gausslemma2dlem0c  26193  2sqlem6  26258  addsqnreup  26278  2sqreulem1  26281  2sqreunnlem1  26284  dchrisumlema  26323  dchrisumlem2  26325  dchrisumlem3  26326  pntlemp  26445  pntleml  26446  ostth3  26473  iscgrglt  26559  colline  26694  axlowdimlem16  27002  axlowdimlem17  27003  axcontlem3  27011  axcontlem10  27018  uhgr2edg  27250  nbupgruvtxres  27449  cusgrres  27490  cusgrfilem2  27498  vdumgr0  27522  frusgrnn0  27613  wlklenvclwlkOLD  27697  wlkp1lem8  27722  pthdivtx  27770  upgrwlkdvde  27778  spthonepeq  27793  usgr2pthlem  27804  lfgrn1cycl  27843  wwlknbp1  27882  wwlknllvtx  27884  wlkiswwlks2lem3  27909  umgr2adedgspth  27986  clwlkclwwlklem3  28038  clwwisshclwwslemlem  28050  clwwisshclwws  28052  clwwlkel  28083  wwlksubclwwlk  28095  eleclclwwlknlem1  28097  eleclclwwlknlem2  28098  erclwwlknref  28106  clwwlknonccat  28133  clwwlknonex2lem2  28145  3wlkdlem4  28199  vdn0conngrumgrv2  28233  eucrctshift  28280  frgrnbnb  28330  frgrncvvdeqlem2  28337  frgrncvvdeqlem3  28338  fusgreghash2wspv  28372  numclwwlk2lem1  28413  numclwlk2lem2f  28414  numclwwlk5  28425  numclwwlk7  28428  frgrreggt1  28430  minvecolem4b  28913  minvecolem4  28915  bcsiALT  29214  ococin  29443  spanpr  29615  pjorthi  29704  nmbdoplbi  30059  nmcoplbi  30063  nmbdfnlbi  30084  nmcfnlbi  30087  nmopcoi  30130  branmfn  30140  hstnmoc  30258  mdsl0  30345  atomli  30417  atcvat4i  30432  atabsi  30436  foresf1o  30523  rabfodom  30524  abrexdomjm  30525  elpreq  30551  ifeqeqx  30558  disjiunel  30608  fovcld  30648  aciunf1lem  30673  ffsrn  30738  xlt2addrd  30755  supxrnemnf  30765  ssnnssfz  30782  dvdszzq  30803  resspos  30917  resstos  30918  gsummptres2  30986  archirngz  31116  orngsqr  31176  isarchiofld  31189  elrspunidl  31274  prmidl2  31284  qsidomlem2  31297  ssmxidl  31310  locfinreflem  31458  cmpcref  31468  fmcncfil  31549  xrge0iifiso  31553  elzdif0  31596  qqhval2lem  31597  esumcst  31697  esumrnmpt2  31702  esumpinfval  31707  esumpinfsum  31711  sigaclci  31766  insiga  31771  ldgenpisys  31800  measres  31856  measdivcstALTV  31859  dya2iocnrect  31914  dya2iocnei  31915  omssubadd  31933  carsggect  31951  carsgclctunlem2  31952  sitgclg  31975  eulerpartlemsv2  31991  eulerpartlemv  31997  eulerpartlemf  32003  eulerpartlemgh  32011  eulerpartlemgs2  32013  ballotlemfp1  32124  ballotlemfrcn0  32162  ftc2re  32244  fdvposlt  32245  fdvposle  32247  bnj1379  32477  bnj580  32560  bnj944  32585  bnj999  32605  bnj1204  32659  bnj1398  32681  cusgredgex  32750  pthacycspth  32786  derangenlem  32800  subfacp1lem3  32811  resconn  32875  cvmliftlem3  32916  satfv0fvfmla0  33042  satfv1fvfmla1  33052  mrsub0  33145  frrlem15  33505  frrlem16  33506  naddssim  33523  sltres  33551  noextenddif  33557  nolesgn2ores  33561  nogesgn1ores  33563  nosep1o  33570  nosep2o  33571  nosepeq  33574  nolt02o  33584  noresle  33586  nosupno  33592  nosupbday  33594  nosupres  33596  nosupbnd1lem1  33597  nosupbnd1lem4  33600  nosupbnd1  33603  nosupbnd2lem1  33604  nosupbnd2  33605  noinfno  33607  noinfbday  33609  noinfres  33611  noinfbnd1lem5  33616  noinfbnd1  33618  noinfbnd2lem1  33619  madebday  33766  cgrextend  33996  segconeq  33998  trisegint  34016  fwddifnp1  34153  ivthALT  34210  fnessref  34232  refssfne  34233  neibastop1  34234  filnetlem4  34256  ontgval  34306  unblimceq0lem  34372  unbdqndv2lem2  34376  unbdqndv2  34377  bj-babygodel  34471  bj-alrimd  34487  bj-exlimd  34492  bj-spcimdv  34767  bj-spcimdvv  34768  bj-finsumval0  35140  bj-fvimacnv0  35141  dfgcd3  35178  relowlssretop  35220  relowlpssretop  35221  onsucuni3  35224  finxpreclem4  35251  poimirlem18  35481  poimirlem21  35484  poimirlem25  35488  ftc1cnnclem  35534  ftc1cnnc  35535  ftc2nc  35545  dvasin  35547  dvacos  35548  abrexdom  35574  indexdom  35578  mettrifi  35601  equivtotbnd  35622  totbndbnd  35633  prdstotbnd  35638  heibor1lem  35653  bfplem1  35666  bfplem2  35667  opidonOLD  35696  rngodm1dm2  35776  zerdivemp1x  35791  equid1  36599  omllaw5N  36947  cmtcomlemN  36948  cmtbr3N  36954  omlfh3N  36959  atlen0  37010  exatleN  37104  hlrelat3  37112  cvrexchlem  37119  atlelt  37138  cvrat4  37143  4atlem11b  37308  4atlem12b  37311  lneq2at  37478  cdlema1N  37491  cdlemblem  37493  paddss12  37519  paddasslem2  37521  paddasslem4  37523  paddasslem6  37525  paddasslem12  37531  paddunN  37627  poml4N  37653  poml5N  37654  osumcllem6N  37661  pexmidlem6N  37675  pl42lem2N  37680  ltrnu  37821  ltrneq2  37848  trlval2  37863  cdlemd6  37903  cdleme25b  38054  cdleme29b  38075  cdlemefr29exN  38102  ltrniotacnvval  38282  cdlemk28-3  38608  dochexmidlem7  39166  muldvds2d  39690  frlmsnic  39916  nna4b4nsq  40141  mzpsubmpt  40209  mzpsubst  40214  eqrabdioph  40243  rabdiophlem2  40268  elpell14qr2  40328  elpell1qr2  40338  pellfundre  40347  pellfundge  40348  pellfundglb  40351  pellfund14gap  40353  congabseq  40440  jm2.22  40461  jm2.23  40462  jm2.26lem3  40467  wepwsolem  40511  dnwech  40517  aomclem2  40524  aomclem4  40526  pwfi2f1o  40565  ss2iundf  40885  dssmapf1od  41247  neik0pk1imk0  41275  gneispace  41362  grur1cld  41464  cpcolld  41490  mnuop23d  41498  mnuprdlem1  41504  mnuprdlem2  41505  mnurndlem1  41513  grumnudlem  41517  radcnvrat  41546  sbiota1  41666  ordelordALT  41771  2pm13.193  41786  ee11an  41924  refsumcn  42187  rfcnnnub  42193  disjxp1  42231  xrnmnfpnf  42247  ssinc  42251  nssd  42269  disjf1o  42343  disjinfi  42345  choicefi  42354  axccdom  42376  dmrelrnrel  42379  monoords  42450  fperiodmullem  42456  xadd0ge  42473  xrssre  42501  xrlexaddrp  42505  xrred  42518  infxr  42520  xrnpnfmnf  42631  monoordxrv  42638  monoord2xrv  42640  fsumsplit1  42731  fsumiunss  42734  fmul01  42739  fmuldfeqlem1  42741  fmuldfeq  42742  fmul01lt1lem1  42743  fmul01lt1lem2  42744  cncfmptss  42746  climinf  42765  climsuselem1  42766  climsuse  42767  limcperiod  42787  limcrecl  42788  sumnnodd  42789  limcleqr  42803  0ellimcdiv  42808  climleltrp  42835  limsuppnfdlem  42860  limsupresxr  42925  liminfresxr  42926  liminfvalxr  42942  cnrefiisplem  42988  xlimmnfvlem1  42991  xlimpnfvlem1  42995  cncfperiod  43038  icccncfext  43046  cncfiooicclem1  43052  dvbdfbdioolem1  43087  dvnmptdivc  43097  dvdsn1add  43098  dvnmptconst  43100  dvnmul  43102  dvmptfprodlem  43103  dvmptfprod  43104  dvnprodlem2  43106  iblspltprt  43132  itgsubsticclem  43134  itgspltprt  43138  itgsbtaddcnst  43141  stoweidlem3  43162  stoweidlem16  43175  stoweidlem17  43176  stoweidlem19  43178  stoweidlem20  43179  stoweidlem23  43182  stoweidlem25  43184  stoweidlem27  43186  stoweidlem31  43190  stoweidlem34  43193  stoweidlem42  43201  stoweidlem48  43207  stoweidlem51  43210  stoweidlem52  43211  stoweidlem59  43218  wallispilem1  43224  wallispilem3  43226  stirlinglem13  43245  fourierdlem16  43282  fourierdlem20  43286  fourierdlem21  43287  fourierdlem38  43304  fourierdlem42  43308  fourierdlem46  43311  fourierdlem48  43313  fourierdlem49  43314  fourierdlem50  43315  fourierdlem54  43319  fourierdlem68  43333  fourierdlem72  43337  fourierdlem73  43338  fourierdlem76  43341  fourierdlem79  43344  fourierdlem81  43346  fourierdlem86  43351  fourierdlem89  43354  fourierdlem90  43355  fourierdlem91  43356  fourierdlem92  43357  fourierdlem97  43362  fourierdlem101  43366  fourierdlem103  43368  fourierdlem104  43369  fourierdlem111  43376  etransclem24  43417  etransclem25  43418  etransclem28  43421  etransclem41  43434  etransclem44  43437  etransclem48  43441  salexct  43491  dfsalgen2  43498  sge0f1o  43538  sge0rnbnd  43549  sge0split  43565  sge0iunmptlemre  43571  sge0fodjrnlem  43572  sge0iunmpt  43574  nnfoctbdjlem  43611  iundjiunlem  43615  meadjiunlem  43621  ismeannd  43623  meaiuninclem  43636  omeiunle  43673  carageniuncllem1  43677  caratheodorylem1  43682  hoidmvlelem4  43754  hoiqssbllem2  43779  salpreimagelt  43860  salpreimalegt  43862  pimdecfgtioc  43867  smfaddlem2  43914  smflimlem6  43926  nsssmfmbflem  43928  smfpimcclem  43955  or2expropbilem1  44141  funressndmfvrn  44153  f1cof1b  44184  2leaddle2  44406  smonoord  44439  uniimaprimaeqfv  44450  fundcmpsurbijinjpreimafv  44475  fundcmpsurinjALT  44480  iccpartf  44499  ich2exprop  44539  ichnreuop  44540  ichreuopeq  44541  sprbisymrel  44567  fmtnodvds  44612  proththdlem  44681  gbowgt5  44830  gboge9  44832  gbege6  44833  stgoldbwt  44844  sbgoldbalt  44849  bgoldbnnsum3prm  44872  isomgrtrlem  44906  uspgrbisymrelALT  44933  ssnn0ssfz  45301  ldepspr  45430  seposep  45835  subthinc  45937  prsthinc  45951  iunord  45996  bnd2d  46001  setrecsss  46020