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  163  jcnd  165  2thd  267  jca  514  syl2anc  586  unitreslOLD  874  aevlem0  2059  equvel  2479  elex2  3516  elex22  3517  spcedv  3599  rspcdf  3610  rspcdva  3625  spsbcd  3786  opth  5368  euotd  5403  wereu2  5552  unielrel  6125  tz7.7  6217  funmo  6371  fvelimad  6732  iinpreima  6837  fnfvima  6995  resfvresima  6997  fliftfun  7065  fliftval  7069  weniso  7107  riota5f  7142  riotass2  7144  ofmpteq  7428  ssorduni  7500  suceloni  7528  nlimsucg  7557  tfisi  7573  zfrep6  7656  curry1  7799  curry2  7802  fnwelem  7825  funsssuppss  7856  wfrlem4  7958  smogt  8004  tfrlem5  8016  omeulem1  8208  oeworde  8219  oelimcl  8226  oeeulem  8227  oeeui  8228  nnawordex  8263  oaabs2  8272  swoso  8322  qliftlem  8378  resixp  8497  undom  8605  xpdom3  8615  domunsncan  8617  omxpenlem  8618  domssex  8678  xpf1o  8679  mapdom3  8689  findcard  8757  f1dmvrnfibi  8808  fiin  8886  marypha1lem  8897  marypha1  8898  fisupcl  8933  supgtoreq  8934  ordiso2  8979  ordtypelem2  8983  ordtypelem8  8989  wemapso2lem  9016  unxpwdom2  9052  cantnflt  9135  cantnfrescl  9139  oemapvali  9147  cantnflem1d  9151  wemapwe  9160  cnfcom  9163  rankr1id  9291  tcrank  9313  cardmin2  9427  infxpenlem  9439  fseqen  9453  ween  9461  ac5num  9462  indcardi  9467  acni2  9472  fodomfi2  9486  infpwfien  9488  inffien  9489  iunfictbso  9540  acacni  9566  dfac12lem2  9570  djuinf  9614  infmap2  9640  ackbij1lem18  9659  ackbij1b  9661  fictb  9667  cfslb2n  9690  cofsmo  9691  cfsmolem  9692  coftr  9695  infpssrlem4  9728  domfin4  9733  fin2i2  9740  isfin2-2  9741  fincssdom  9745  ssfin3ds  9752  fin23lem20  9759  fin23lem30  9764  isf32lem3  9777  fin1a2lem12  9833  fin1a2lem13  9834  hsmexlem2  9849  axdc2lem  9870  imadomg  9956  fnct  9959  iundom2g  9962  iundomg  9963  iundom  9964  unirnfdomd  9989  konigthlem  9990  iunctb  9996  fpwwe2  10065  canthwelem  10072  pwfseqlem3  10082  pwfseqlem5  10085  winalim2  10118  wunelss  10130  r1wunlim  10159  wunex2  10160  tsksdom  10178  tskinf  10191  inttsk  10196  inar1  10197  tskcard  10203  tskurn  10211  gruina  10240  grur1a  10241  grur1  10242  addsrpr  10497  mulsrpr  10498  lemul12a  11498  lemulge11  11502  lediv12a  11533  nngt0  11669  nn0ge2m1nn  11965  peano5uzi  12072  nn0ind-raph  12083  znnn0nn  12095  suprzub  12340  uzsupss  12341  rpge0  12403  fz0fzelfz0  13014  fz0fzdiffz0  13017  ige2m2fzo  13101  elfzodifsumelfzo  13104  elfzom1elp1fzo  13105  fzonfzoufzol  13141  flltdivnn0lt  13204  fldiv  13229  modaddmodup  13303  uzrdgsuci  13329  fzennn  13337  uzindi  13351  fsuppmapnn0fiubex  13361  expcl2lem  13442  leexp1a  13540  modexp  13600  faclbnd  13651  faclbnd6  13660  facavg  13662  hashginv  13695  hashf1rn  13714  hasheqf1od  13715  seqcoll  13823  hashge2el2dif  13839  wrdsymb0  13901  wrdlenge2n0  13904  ccatsymb  13936  swrdnd2  14017  swrdnd0  14019  pfxnd  14049  pfxccat1  14064  swrdpfx  14069  pfxpfx  14070  wrd2ind  14085  pfxccatin12  14095  pfxccat3  14096  swrdccat  14097  pfxccatpfx1  14098  pfxccatpfx2  14099  swrdccatin1d  14105  pfxccatin12d  14107  repswswrd  14146  cshwidxmod  14165  s2f1o  14278  f1oun2prg  14279  wwlktovfo  14322  relexpreld  14399  relexpfld  14408  rtrclreclem3  14419  resqrex  14610  cau3lem  14714  reusq0  14822  rlimcld2  14935  climcn2  14949  isercoll  15024  climsup  15026  caurcvgr  15030  sumeq2ii  15050  summolem3  15071  zsum  15075  fsumadd  15096  fsum2dlem  15125  fsum0diag2  15138  fsummulc2  15139  fsumabs  15156  fsumrelem  15162  fsumrlim  15166  fsumo1  15167  o1fsum  15168  fsumiun  15176  qshash  15182  prodeq2ii  15267  prodmolem3  15287  fprodmul  15314  fproddiv  15315  fprod2dlem  15334  fprodsplit1f  15344  sin02gt0  15545  efieq1re  15552  p1modz1  15614  dvdsleabs2  15662  4dvdseven  15724  sumeven  15738  sumodd  15739  divalglem9  15752  smupvallem  15832  rppwr  15908  algfx  15924  eucalgcvga  15930  lcmfunsnlem1  15981  lcmfunsnlem2lem1  15982  lcmflefac  15992  qredeq  16001  fermltl  16121  modprm0  16142  pythagtriplem4  16156  pythagtriplem6  16158  pythagtriplem7  16159  pythagtriplem12  16163  pythagtriplem13  16164  pythagtriplem14  16165  pythagtriplem16  16167  difsqpwdvds  16223  pcmpt  16228  prmreclem2  16253  4sqlem11  16291  vdwlem9  16325  vdwlem11  16327  vdwlem12  16328  0ram  16356  0ram2  16357  0ramcl  16359  ramcl  16365  prmolelcmf  16384  cshwsidrepsw  16427  cshwshashlem2  16430  prmlem1  16441  prmlem2  16453  strfvd  16528  strfv2d  16529  strssd  16533  firest  16706  prdsdsval3  16758  imasbas  16785  imasds  16786  imasaddfnlem  16801  imasaddvallem  16802  imasvscafn  16810  qusaddvallem  16824  qusaddflem  16825  qusaddval  16826  qusaddf  16827  qusmulval  16828  qusmulf  16829  catideu  16946  idinv  17059  brcici  17070  invfuc  17244  2initoinv  17270  initoeu1w  17272  initoeu2lem0  17273  2termoinv  17277  termoeu1w  17279  mod2ile  17716  lubss  17731  acsmapd  17788  lidrididd  17880  gsumval2a  17895  mndind  17992  submefmnd  18060  mgm2nsgrplem4  18086  qusgrp2  18217  mulgnegnn  18238  pgrpsubgsymg  18537  fvcosymgeq  18557  gsmsymgreqlem1  18558  psgnunilem4  18625  pgpssslw  18739  sylow2alem2  18743  fislw  18750  efgsres  18864  rinvmod  18929  gsumval3lem2  19026  gsumzaddlem  19041  gsum2d  19092  nn0gsumfz  19104  telgsums  19113  dprddomcld  19123  ablfac2  19211  srgi  19261  ringi  19310  qusring2  19370  lssintcl  19736  lbsextlem3  19932  lbsextlem4  19933  evlseu  20296  mptcoe1fsupp  20383  cply1coe0bi  20468  mpfpf1  20514  pf1mpf  20515  zringlpirlem3  20633  psgnodpm  20732  psgndiflemB  20744  frlmup4  20945  lindff1  20964  lindfrn  20965  lmisfree  20986  mat0dimscm  21078  mdetdiagid  21209  mdet1  21210  mdetunilem9  21229  slesolinv  21289  cramerimp  21295  cpmatmcllem  21326  mptcoe1matfsupp  21410  mp2pm2mp  21419  chpdmat  21449  cctop  21614  subbascn  21862  cnss2  21885  cmpcovf  21999  2ndcctbss  22063  2ndcomap  22066  2ndcsep  22067  comppfsc  22140  ptclsg  22223  dfac14  22226  txcnp  22228  ptcnplem  22229  uptx  22233  txtube  22248  tx2ndc  22259  xkococnlem  22267  elqtop  22305  qtoprest  22325  indishmph  22406  ptcmpfi  22421  kqhmph  22427  csdfil  22502  filssufilg  22519  ufilen  22538  rnelfm  22561  fmfnfmlem4  22565  alexsubALTlem4  22658  ptcmplem4  22663  cnextfvval  22673  cnextcn  22675  cnextfres  22677  tmdgsum2  22704  imasf1oxmet  22985  metss  23118  met2ndci  23132  prdsxmslem2  23139  metust  23168  cfilucfil  23169  metustbl  23176  psmetutop  23177  opnreen  23439  rectbntr0  23440  fsumcn  23478  rescncf  23505  xrhmeo  23550  cnllycmp  23560  lebnumlem1  23565  lebnumlem3  23567  cfilss  23873  iscmet3lem1  23894  iscmet3lem2  23895  ivthicc  24059  ovolsslem  24085  ovoliunlem2  24104  ovoliunnul  24108  ovolicc2lem4  24121  voliunlem3  24153  volsup  24157  uniiccdif  24179  uniioombllem2  24184  volivth  24208  mbfimaopnlem  24256  mbflimsup  24267  i1fd  24282  itg1addlem4  24300  itg2addlem  24359  itg2gt0  24361  limciun  24492  dvadd  24537  dvmul  24538  dvco  24544  dvrec  24552  dvcnv  24574  dvferm  24585  rollelem  24586  dvlip  24590  dvlip2  24592  c1liplem1  24593  c1lip2  24595  dvgt0lem1  24599  dvivthlem1  24605  lhop1lem  24610  dvcnvrelem1  24614  dvcnvrelem2  24615  dvcvx  24617  dvfsumle  24618  dvfsumabs  24620  dvfsumlem1  24623  dvfsumlem2  24624  dvfsumlem4  24626  dvfsumrlim2  24629  dvfsum2  24631  ftc1cn  24640  ftc2ditglem  24642  itgsubstlem  24645  tdeglem4  24654  mdegaddle  24668  mdegmullem  24672  deg1sublt  24704  ply1divmo  24729  fta1g  24761  dgrub  24824  dgrnznn  24837  dgradd2  24858  dvply1  24873  plyrem  24894  aalioulem4  24924  aalioulem5  24925  aalioulem6  24926  aaliou2  24929  taylf  24949  ulmdv  24991  psercn2  25011  abelth  25029  abelth2  25030  reeff1olem  25034  efopn  25241  logreclem  25340  isosctrlem2  25397  xrlimcnp  25546  basellem4  25661  ppiwordi  25739  musum  25768  chpub  25796  gausslemma2dlem0c  25934  2sqlem6  25999  addsqnreup  26019  2sqreulem1  26022  2sqreunnlem1  26025  dchrisumlema  26064  dchrisumlem2  26066  dchrisumlem3  26067  pntlemp  26186  pntleml  26187  ostth3  26214  iscgrglt  26300  colline  26435  axlowdimlem16  26743  axlowdimlem17  26744  axcontlem3  26752  axcontlem10  26759  uhgr2edg  26990  nbupgruvtxres  27189  cusgrres  27230  cusgrfilem2  27238  vdumgr0  27262  frusgrnn0  27353  wlklenvclwlkOLD  27437  wlkp1lem8  27462  pthdivtx  27510  upgrwlkdvde  27518  spthonepeq  27533  usgr2pthlem  27544  lfgrn1cycl  27583  wwlknbp1  27622  wwlknllvtx  27624  wlkiswwlks2lem3  27649  umgr2adedgspth  27727  clwlkclwwlklem3  27779  clwwisshclwwslemlem  27791  clwwisshclwws  27793  clwwlkel  27825  wwlksubclwwlk  27837  eleclclwwlknlem1  27839  eleclclwwlknlem2  27840  erclwwlknref  27848  clwwlknonccat  27875  clwwlknonex2lem2  27887  3wlkdlem4  27941  vdn0conngrumgrv2  27975  eucrctshift  28022  frgrnbnb  28072  frgrncvvdeqlem2  28079  frgrncvvdeqlem3  28080  fusgreghash2wspv  28114  numclwwlk2lem1  28155  numclwlk2lem2f  28156  numclwwlk5  28167  numclwwlk7  28170  frgrreggt1  28172  minvecolem4b  28655  minvecolem4  28657  bcsiALT  28956  ococin  29185  spanpr  29357  pjorthi  29446  nmbdoplbi  29801  nmcoplbi  29805  nmbdfnlbi  29826  nmcfnlbi  29829  nmopcoi  29872  branmfn  29882  hstnmoc  30000  mdsl0  30087  atomli  30159  atcvat4i  30174  atabsi  30178  foresf1o  30265  rabfodom  30266  abrexdomjm  30267  elpreq  30290  ifeqeqx  30297  disjiunel  30346  fovcld  30385  aciunf1lem  30407  ffsrn  30465  xlt2addrd  30482  supxrnemnf  30493  ssnnssfz  30510  dvdszzq  30531  resspos  30646  resstos  30647  archirngz  30818  orngsqr  30877  isarchiofld  30890  prmidl2  30958  qsidomlem2  30966  ssmxidl  30979  locfinreflem  31104  cmpcref  31114  fmcncfil  31174  xrge0iifiso  31178  elzdif0  31221  qqhval2lem  31222  esumcst  31322  esumrnmpt2  31327  esumpinfval  31332  esumpinfsum  31336  sigaclci  31391  insiga  31396  ldgenpisys  31425  measres  31481  measdivcstALTV  31484  dya2iocnrect  31539  dya2iocnei  31540  omssubadd  31558  carsggect  31576  carsgclctunlem2  31577  sitgclg  31600  eulerpartlemsv2  31616  eulerpartlemv  31622  eulerpartlemf  31628  eulerpartlemgh  31636  eulerpartlemgs2  31638  ballotlemfp1  31749  ballotlemfrcn0  31787  ftc2re  31869  fdvposlt  31870  fdvposle  31872  bnj1379  32102  bnj580  32185  bnj944  32210  bnj999  32230  bnj1204  32284  bnj1398  32306  cusgredgex  32368  pthacycspth  32404  derangenlem  32418  subfacp1lem3  32429  subfacp1lem5  32431  resconn  32493  cvmliftlem3  32534  satfv0fvfmla0  32660  satfv1fvfmla1  32670  mrsub0  32763  frpomin  33078  frrlem4  33126  frrlem8  33130  frrlem10  33132  fprlem1  33137  fprlem2  33138  frrlem15  33142  frrlem16  33143  sltres  33169  noextenddif  33175  nolesgn2ores  33179  nosep1o  33186  nosepeq  33189  nolt02o  33199  noresle  33200  nosupno  33203  nosupres  33207  nosupbnd1lem1  33208  nosupbnd1lem4  33211  nosupbnd1  33214  nosupbnd2lem1  33215  nosupbnd2  33216  sslttr  33268  cgrextend  33469  segconeq  33471  trisegint  33489  fwddifnp1  33626  ivthALT  33683  fnessref  33705  refssfne  33706  neibastop1  33707  filnetlem4  33729  ontgval  33779  unblimceq0lem  33845  unbdqndv2lem2  33849  unbdqndv2  33850  bj-babygodel  33937  bj-alrimd  33953  bj-exlimd  33958  bj-spcimdv  34214  bj-spcimdvv  34215  bj-finsumval0  34570  bj-fvimacnv0  34571  dfgcd3  34608  relowlssretop  34647  relowlpssretop  34648  onsucuni3  34651  finxpreclem4  34678  poimirlem18  34925  poimirlem21  34928  poimirlem25  34932  ftc1cnnclem  34980  ftc1cnnc  34981  ftc2nc  34991  dvasin  34993  dvacos  34994  abrexdom  35020  indexdom  35024  mettrifi  35047  equivtotbnd  35071  totbndbnd  35082  prdstotbnd  35087  heibor1lem  35102  bfplem1  35115  bfplem2  35116  opidonOLD  35145  rngodm1dm2  35225  zerdivemp1x  35240  equid1  36050  omllaw5N  36398  cmtcomlemN  36399  cmtbr3N  36405  omlfh3N  36410  atlen0  36461  exatleN  36555  hlrelat3  36563  cvrexchlem  36570  atlelt  36589  cvrat4  36594  4atlem11b  36759  4atlem12b  36762  lneq2at  36929  cdlema1N  36942  cdlemblem  36944  paddss12  36970  paddasslem2  36972  paddasslem4  36974  paddasslem6  36976  paddasslem12  36982  paddunN  37078  poml4N  37104  poml5N  37105  osumcllem6N  37112  pexmidlem6N  37126  pl42lem2N  37131  ltrnu  37272  ltrneq2  37299  trlval2  37314  cdlemd6  37354  cdleme25b  37505  cdleme29b  37526  cdlemefr29exN  37553  ltrniotacnvval  37733  cdlemk28-3  38059  dochexmidlem7  38617  frlmsnic  39169  mzpsubmpt  39360  mzpsubst  39365  eqrabdioph  39394  rabdiophlem2  39419  elpell14qr2  39479  elpell1qr2  39489  pellfundre  39498  pellfundge  39499  pellfundglb  39502  pellfund14gap  39504  congabseq  39591  jm2.22  39612  jm2.23  39613  jm2.26lem3  39618  wepwsolem  39662  dnwech  39668  aomclem2  39675  aomclem4  39677  pwfi2f1o  39716  itgpowd  39841  ss2iundf  40024  dssmapf1od  40387  neik0pk1imk0  40417  gneispace  40504  grur1cld  40588  cpcolld  40614  mnuop23d  40622  mnuprdlem1  40628  mnuprdlem2  40629  mnurndlem1  40637  grumnudlem  40641  radcnvrat  40666  sbiota1  40786  ordelordALT  40891  2pm13.193  40906  ee11an  41044  refsumcn  41307  rfcnnnub  41313  disjxp1  41351  xrnmnfpnf  41367  ssinc  41373  nssd  41391  ralimda  41426  disjf1o  41472  disjinfi  41474  choicefi  41483  axccdom  41507  dmrelrnrel  41510  monoords  41584  fperiodmullem  41590  xadd0ge  41608  xrssre  41636  xrlexaddrp  41640  xrred  41653  infxr  41655  fiminre2  41666  xrnpnfmnf  41771  monoordxrv  41778  monoord2xrv  41780  fsumsplit1  41873  fsumiunss  41876  fmul01  41881  fmuldfeqlem1  41883  fmuldfeq  41884  fmul01lt1lem1  41885  fmul01lt1lem2  41886  cncfmptss  41888  climinf  41907  climsuselem1  41908  climsuse  41909  limcperiod  41929  limcrecl  41930  sumnnodd  41931  limcleqr  41945  0ellimcdiv  41950  climleltrp  41977  limsuppnfdlem  42002  limsupresxr  42067  liminfresxr  42068  liminfvalxr  42084  cnrefiisplem  42130  xlimmnfvlem1  42133  xlimpnfvlem1  42137  cncfperiod  42182  icccncfext  42190  cncfiooicclem1  42196  dvbdfbdioolem1  42233  dvnmptdivc  42243  dvdsn1add  42244  dvnmptconst  42246  dvnmul  42248  dvmptfprodlem  42249  dvmptfprod  42250  dvnprodlem2  42252  iblspltprt  42278  itgsubsticclem  42280  itgspltprt  42284  itgsbtaddcnst  42287  stoweidlem3  42308  stoweidlem16  42321  stoweidlem17  42322  stoweidlem19  42324  stoweidlem20  42325  stoweidlem23  42328  stoweidlem25  42330  stoweidlem27  42332  stoweidlem31  42336  stoweidlem34  42339  stoweidlem42  42347  stoweidlem48  42353  stoweidlem51  42356  stoweidlem52  42357  stoweidlem59  42364  wallispilem1  42370  wallispilem3  42372  stirlinglem13  42391  fourierdlem16  42428  fourierdlem20  42432  fourierdlem21  42433  fourierdlem38  42450  fourierdlem42  42454  fourierdlem46  42457  fourierdlem48  42459  fourierdlem49  42460  fourierdlem50  42461  fourierdlem54  42465  fourierdlem68  42479  fourierdlem72  42483  fourierdlem73  42484  fourierdlem76  42487  fourierdlem79  42490  fourierdlem81  42492  fourierdlem86  42497  fourierdlem89  42500  fourierdlem90  42501  fourierdlem91  42502  fourierdlem92  42503  fourierdlem97  42508  fourierdlem101  42512  fourierdlem103  42514  fourierdlem104  42515  fourierdlem111  42522  etransclem24  42563  etransclem25  42564  etransclem28  42567  etransclem41  42580  etransclem44  42583  etransclem48  42587  salexct  42637  dfsalgen2  42644  sge0f1o  42684  sge0rnbnd  42695  sge0split  42711  sge0iunmptlemre  42717  sge0fodjrnlem  42718  sge0iunmpt  42720  nnfoctbdjlem  42757  iundjiunlem  42761  meadjiunlem  42767  ismeannd  42769  meaiuninclem  42782  omeiunle  42819  carageniuncllem1  42823  caratheodorylem1  42828  hoidmvlelem4  42900  hoiqssbllem2  42925  salpreimagelt  43006  salpreimalegt  43008  pimdecfgtioc  43013  smfaddlem2  43060  smflimlem6  43072  nsssmfmbflem  43074  smfpimcclem  43101  or2expropbilem1  43287  funressndmfvrn  43299  2leaddle2  43518  smonoord  43551  uniimaprimaeqfv  43562  fundcmpsurbijinjpreimafv  43587  fundcmpsurinjALT  43592  iccpartf  43611  ich2exprop  43653  ichnreuop  43654  ichreuopeq  43655  sprbisymrel  43681  fmtnodvds  43726  proththdlem  43798  gbowgt5  43947  gboge9  43949  gbege6  43950  stgoldbwt  43961  sbgoldbalt  43966  bgoldbnnsum3prm  43989  isomgrtrlem  44023  uspgrbisymrelALT  44050  ssnn0ssfz  44417  ldepspr  44548  iunord  44799  bnd2d  44804  setrecsss  44823