MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylc Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 sylc.1 . . 3 (𝜑𝜓)
2 sylc.2 . . 3 (𝜑𝜒)
3 sylc.3 . . 3 (𝜓 → (𝜒𝜃))
41, 2, 3syl2im 40 . 2 (𝜑 → (𝜑𝜃))
54pm2.43i 52 1 (𝜑𝜃)
Colors of variables: wff setvar class
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  876  aevlem0  2057  equvel  2454  elex2OLD  3464  elex22  3465  spcedv  3555  rspcdf  3566  rspcdva  3580  spsbcd  3751  opth  5431  euotd  5468  wereu2  5628  unielrel  6224  frpomin  6292  tz7.7  6341  funmo  6513  funmoOLD  6514  fvelimad  6906  iinpreima  7016  fnfvima  7179  resfvresima  7181  fliftfun  7253  fliftval  7257  weniso  7295  riota5f  7338  riotass2  7340  ofmpteq  7635  ssorduni  7709  sucexeloniOLD  7741  suceloniOLD  7743  nlimsucg  7774  tfisi  7791  zfrep6  7883  curry1  8032  curry2  8035  fnwelem  8059  funsssuppss  8117  frrlem4  8216  frrlem8  8220  frrlem10  8222  fprlem1  8227  fprlem2  8228  wfrlem4OLD  8254  smogt  8309  tfrlem5  8322  omeulem1  8525  oeworde  8536  oelimcl  8543  oeeulem  8544  oeeui  8545  nnawordex  8580  oaabs2  8591  naddssim  8626  swoso  8677  qliftlem  8733  resixp  8867  domssl  8934  domssr  8935  undomOLD  9000  xpdom3  9010  domunsncan  9012  omxpenlem  9013  domssex  9078  xpf1o  9079  mapdom3  9089  dif1en  9100  findcard  9103  f1dmvrnfibi  9276  fiin  9354  marypha1lem  9365  marypha1  9366  fisupcl  9401  supgtoreq  9402  ordiso2  9447  ordtypelem2  9451  ordtypelem8  9457  wemapso2lem  9484  unxpwdom2  9520  cantnflt  9604  cantnfrescl  9608  oemapvali  9616  cantnflem1d  9620  wemapwe  9629  cnfcom  9632  ttrclss  9652  ttrclselem2  9658  frrlem15  9689  rankr1id  9794  tcrank  9816  cardmin2  9931  infxpenlem  9945  fseqen  9959  ween  9967  ac5num  9968  indcardi  9973  acni2  9978  fodomfi2  9992  infpwfien  9994  inffien  9995  iunfictbso  10046  acacni  10072  dfac12lem2  10076  djuinf  10120  infmap2  10150  ackbij1lem18  10169  ackbij1b  10171  fictb  10177  cfslb2n  10200  cofsmo  10201  cfsmolem  10202  coftr  10205  infpssrlem4  10238  domfin4  10243  fin2i2  10250  isfin2-2  10251  fincssdom  10255  ssfin3ds  10262  fin23lem20  10269  fin23lem30  10274  isf32lem3  10287  fin1a2lem12  10343  fin1a2lem13  10344  hsmexlem2  10359  axdc2lem  10380  imadomg  10466  fnct  10469  iundom2g  10472  iundomg  10473  iundom  10474  unirnfdomd  10499  konigthlem  10500  iunctb  10506  fpwwe2  10575  canthwelem  10582  pwfseqlem3  10592  pwfseqlem5  10595  winalim2  10628  wunelss  10640  r1wunlim  10669  wunex2  10670  tsksdom  10688  tskinf  10701  inttsk  10706  inar1  10707  tskcard  10713  tskurn  10721  gruina  10750  grur1a  10751  grur1  10752  addsrpr  11007  mulsrpr  11008  lemul12a  12009  lemulge11  12013  lediv12a  12044  fiminre2  12099  nngt0  12180  nn0ge2m1nn  12478  peano5uzi  12588  nn0ind-raph  12599  znnn0nn  12610  suprzub  12856  uzsupss  12857  rpge0  12920  fz0fzelfz0  13539  fz0fzdiffz0  13542  ige2m2fzo  13627  elfzodifsumelfzo  13630  elfzom1elp1fzo  13631  fzonfzoufzol  13667  flltdivnn0lt  13730  fldiv  13757  modaddmodup  13831  uzrdgsuci  13857  fzennn  13865  uzindi  13879  fsuppmapnn0fiubex  13889  expcl2lem  13971  leexp1a  14072  modexp  14133  faclbnd  14182  faclbnd6  14191  facavg  14193  hashginv  14226  hashf1rn  14244  hasheqf1od  14245  seqcoll  14355  hashge2el2dif  14371  wrdsymb0  14429  wrdlenge2n0  14432  ccatsymb  14462  swrdnd2  14535  swrdnd0  14537  pfxnd  14567  pfxccat1  14582  swrdpfx  14587  pfxpfx  14588  wrd2ind  14603  pfxccatin12  14613  pfxccat3  14614  swrdccat  14615  pfxccatpfx1  14616  pfxccatpfx2  14617  swrdccatin1d  14623  pfxccatin12d  14625  repswswrd  14664  cshwidxmod  14683  s2f1o  14797  f1oun2prg  14798  wwlktovfo  14839  relexpfld  14926  rtrclreclem3  14937  resqrex  15127  cau3lem  15231  reusq0  15339  rlimcld2  15452  climcn2  15467  isercoll  15544  climsup  15546  caurcvgr  15550  sumeq2ii  15570  summolem3  15591  zsum  15595  fsumadd  15617  fsumsplit1  15622  fsum2dlem  15647  fsum0diag2  15660  fsummulc2  15661  fsumabs  15678  fsumrelem  15684  fsumrlim  15688  fsumo1  15689  o1fsum  15690  fsumiun  15698  qshash  15704  prodeq2ii  15788  prodmolem3  15808  fprodmul  15835  fproddiv  15836  fprod2dlem  15855  fprodsplit1f  15865  sin02gt0  16066  efieq1re  16073  p1modz1  16135  dvdsleabs2  16186  4dvdseven  16247  sumeven  16261  sumodd  16262  divalglem9  16275  smupvallem  16355  algfx  16448  eucalgcvga  16454  lcmfunsnlem1  16505  lcmfunsnlem2lem1  16506  lcmflefac  16516  qredeq  16525  fermltl  16648  modprm0  16669  pythagtriplem4  16683  pythagtriplem6  16685  pythagtriplem7  16686  pythagtriplem12  16690  pythagtriplem13  16691  pythagtriplem14  16692  pythagtriplem16  16694  difsqpwdvds  16751  pcmpt  16756  prmreclem2  16781  4sqlem11  16819  vdwlem9  16853  vdwlem11  16855  vdwlem12  16856  0ram  16884  0ram2  16885  0ramcl  16887  ramcl  16893  prmolelcmf  16912  cshwsidrepsw  16958  cshwshashlem2  16961  prmlem1  16972  prmlem2  16984  strfvd  17065  strfv2d  17066  strssd  17070  firest  17306  prdsdsval3  17359  imasbas  17386  imasds  17387  imasaddfnlem  17402  imasaddvallem  17403  imasvscafn  17411  qusaddvallem  17425  qusaddflem  17426  qusaddval  17427  qusaddf  17428  qusmulval  17429  qusmulf  17430  catideu  17547  idinv  17664  brcici  17675  invfuc  17855  2initoinv  17888  initoeu1w  17890  initoeu2lem0  17891  2termoinv  17895  termoeu1w  17897  mod2ile  18375  lubss  18394  acsmapd  18435  lidrididd  18517  gsumval2a  18532  mndind  18630  submefmnd  18697  mgm2nsgrplem4  18723  qusgrp2  18856  mulgnegnn  18877  pgrpsubgsymg  19182  fvcosymgeq  19202  gsmsymgreqlem1  19203  psgnunilem4  19270  pgpssslw  19387  sylow2alem2  19391  fislw  19398  efgsres  19511  rinvmod  19578  gsumval3lem2  19674  gsumzaddlem  19689  gsum2d  19740  nn0gsumfz  19752  telgsums  19761  dprddomcld  19771  ablfac2  19859  srgdilem  19914  ringdilem  19966  qusring2  20031  lssintcl  20410  lbsextlem3  20606  lbsextlem4  20607  zringlpirlem3  20870  psgnodpm  20977  psgndiflemB  20989  frlmup4  21192  lindff1  21211  lindfrn  21212  lmisfree  21233  evlseu  21477  mhpmulcl  21523  mptcoe1fsupp  21570  cply1coe0bi  21655  mpfpf1  21701  pf1mpf  21702  mat0dimscm  21802  mdetdiagid  21933  mdet1  21934  mdetunilem9  21953  slesolinv  22013  cramerimp  22019  cpmatmcllem  22051  mptcoe1matfsupp  22135  mp2pm2mp  22144  chpdmat  22174  cctop  22340  subbascn  22589  cnss2  22612  cmpcovf  22726  2ndcctbss  22790  2ndcomap  22793  2ndcsep  22794  comppfsc  22867  ptclsg  22950  dfac14  22953  txcnp  22955  ptcnplem  22956  uptx  22960  txtube  22975  tx2ndc  22986  xkococnlem  22994  elqtop  23032  qtoprest  23052  indishmph  23133  ptcmpfi  23148  kqhmph  23154  csdfil  23229  filssufilg  23246  ufilen  23265  rnelfm  23288  fmfnfmlem4  23292  alexsubALTlem4  23385  ptcmplem4  23390  cnextfvval  23400  cnextcn  23402  cnextfres  23404  tmdgsum2  23431  imasf1oxmet  23712  metss  23848  met2ndci  23862  prdsxmslem2  23869  metust  23898  cfilucfil  23899  metustbl  23906  psmetutop  23907  opnreen  24178  rectbntr0  24179  fsumcn  24217  rescncf  24244  xrhmeo  24293  cnllycmp  24303  lebnumlem1  24308  lebnumlem3  24310  cfilss  24618  iscmet3lem1  24639  iscmet3lem2  24640  ivthicc  24806  ovolsslem  24832  ovoliunlem2  24851  ovoliunnul  24855  ovolicc2lem4  24868  voliunlem3  24900  volsup  24904  uniiccdif  24926  uniioombllem2  24931  volivth  24955  mbfimaopnlem  25003  mbflimsup  25014  i1fd  25029  itg1addlem4  25047  itg1addlem4OLD  25048  itg2addlem  25107  itg2gt0  25109  limciun  25242  dvadd  25288  dvmul  25289  dvco  25295  dvrec  25303  dvcnv  25325  dvferm  25336  rollelem  25337  dvlip  25341  dvlip2  25343  c1liplem1  25344  c1lip2  25346  dvgt0lem1  25350  dvivthlem1  25356  lhop1lem  25361  dvcnvrelem1  25365  dvcnvrelem2  25366  dvcvx  25368  dvfsumle  25369  dvfsumabs  25371  dvfsumlem1  25374  dvfsumlem2  25375  dvfsumlem4  25377  dvfsumrlim2  25380  dvfsum2  25382  ftc1cn  25391  ftc2ditglem  25393  itgsubstlem  25396  itgpowd  25398  tdeglem4OLD  25409  mdegaddle  25423  mdegmullem  25427  deg1sublt  25459  ply1divmo  25484  fta1g  25516  dgrub  25579  dgrnznn  25592  dgradd2  25613  dvply1  25628  plyrem  25649  aalioulem4  25679  aalioulem5  25680  aalioulem6  25681  aaliou2  25684  taylf  25704  ulmdv  25746  psercn2  25766  abelth  25784  abelth2  25785  reeff1olem  25789  efopn  25997  logreclem  26096  isosctrlem2  26153  xrlimcnp  26302  basellem4  26417  ppiwordi  26495  musum  26524  chpub  26552  gausslemma2dlem0c  26690  2sqlem6  26755  addsqnreup  26775  2sqreulem1  26778  2sqreunnlem1  26781  dchrisumlema  26820  dchrisumlem2  26822  dchrisumlem3  26823  pntlemp  26942  pntleml  26943  ostth3  26970  sltres  26994  noextenddif  27000  nolesgn2ores  27004  nogesgn1ores  27006  nosep1o  27013  nosep2o  27014  nosepeq  27017  nolt02o  27027  noresle  27029  nosupno  27035  nosupbday  27037  nosupres  27039  nosupbnd1lem1  27040  nosupbnd1lem4  27043  nosupbnd1  27046  nosupbnd2lem1  27047  nosupbnd2  27048  noinfno  27050  noinfbday  27052  noinfres  27054  noinfbnd1lem5  27059  noinfbnd1  27061  noinfbnd2lem1  27062  madebday  27213  iscgrglt  27342  colline  27477  axlowdimlem16  27792  axlowdimlem17  27793  axcontlem3  27801  axcontlem10  27808  uhgr2edg  28042  nbupgruvtxres  28241  cusgrres  28282  cusgrfilem2  28290  vdumgr0  28314  frusgrnn0  28405  wlkp1lem8  28514  pthdivtx  28563  upgrwlkdvde  28571  spthonepeq  28586  usgr2pthlem  28597  lfgrn1cycl  28636  wwlknbp1  28675  wwlknllvtx  28677  wlkiswwlks2lem3  28702  umgr2adedgspth  28779  clwlkclwwlklem3  28831  clwwisshclwwslemlem  28843  clwwisshclwws  28845  clwwlkel  28876  wwlksubclwwlk  28888  eleclclwwlknlem1  28890  eleclclwwlknlem2  28891  erclwwlknref  28899  clwwlknonccat  28926  clwwlknonex2lem2  28938  3wlkdlem4  28992  vdn0conngrumgrv2  29026  eucrctshift  29073  frgrnbnb  29123  frgrncvvdeqlem2  29130  frgrncvvdeqlem3  29131  fusgreghash2wspv  29165  numclwwlk2lem1  29206  numclwlk2lem2f  29207  numclwwlk5  29218  numclwwlk7  29221  frgrreggt1  29223  minvecolem4b  29706  minvecolem4  29708  bcsiALT  30007  ococin  30236  spanpr  30408  pjorthi  30497  nmbdoplbi  30852  nmcoplbi  30856  nmbdfnlbi  30877  nmcfnlbi  30880  nmopcoi  30923  branmfn  30933  hstnmoc  31051  mdsl0  31138  atomli  31210  atcvat4i  31225  atabsi  31229  foresf1o  31317  rabfodom  31318  abrexdomjm  31319  elpreq  31343  ifeqeqx  31350  disjiunel  31400  fovcld  31440  aciunf1lem  31464  ffsrn  31529  xlt2addrd  31546  supxrnemnf  31556  ssnnssfz  31573  dvdszzq  31594  resspos  31709  resstos  31710  gsummptres2  31778  archirngz  31908  orngsqr  31982  isarchiofld  31995  elrspunidl  32082  prmidl2  32092  qsidomlem2  32105  ssmxidl  32118  locfinreflem  32290  cmpcref  32300  fmcncfil  32381  xrge0iifiso  32385  elzdif0  32430  qqhval2lem  32431  esumcst  32531  esumrnmpt2  32536  esumpinfval  32541  esumpinfsum  32545  sigaclci  32600  insiga  32605  ldgenpisys  32634  measres  32690  measdivcstALTV  32693  dya2iocnrect  32750  dya2iocnei  32751  omssubadd  32769  carsggect  32787  carsgclctunlem2  32788  sitgclg  32811  eulerpartlemsv2  32827  eulerpartlemv  32833  eulerpartlemf  32839  eulerpartlemgh  32847  eulerpartlemgs2  32849  ballotlemfp1  32960  ballotlemfrcn0  32998  ftc2re  33080  fdvposlt  33081  fdvposle  33083  bnj1379  33311  bnj580  33394  bnj944  33419  bnj999  33439  bnj1204  33493  bnj1398  33515  cusgredgex  33584  pthacycspth  33620  derangenlem  33634  subfacp1lem3  33645  resconn  33709  cvmliftlem3  33750  satfv0fvfmla0  33876  satfv1fvfmla1  33886  mrsub0  33979  sleadd1  34302  cgrextend  34560  segconeq  34562  trisegint  34580  fwddifnp1  34717  ivthALT  34774  fnessref  34796  refssfne  34797  neibastop1  34798  filnetlem4  34820  ontgval  34870  unblimceq0lem  34936  unbdqndv2lem2  34940  unbdqndv2  34941  bj-babygodel  35035  bj-alrimd  35051  bj-exlimd  35056  bj-spcimdv  35329  bj-spcimdvv  35330  bj-finsumval0  35723  bj-fvimacnv0  35724  dfgcd3  35762  relowlssretop  35801  relowlpssretop  35802  onsucuni3  35805  finxpreclem4  35832  poimirlem18  36063  poimirlem21  36066  poimirlem25  36070  ftc1cnnclem  36116  ftc1cnnc  36117  ftc2nc  36127  dvasin  36129  dvacos  36130  abrexdom  36156  indexdom  36160  mettrifi  36183  equivtotbnd  36204  totbndbnd  36215  prdstotbnd  36220  heibor1lem  36235  bfplem1  36248  bfplem2  36249  opidonOLD  36278  rngodm1dm2  36358  zerdivemp1x  36373  equid1  37328  omllaw5N  37676  cmtcomlemN  37677  cmtbr3N  37683  omlfh3N  37688  atlen0  37739  exatleN  37834  hlrelat3  37842  cvrexchlem  37849  atlelt  37868  cvrat4  37873  4atlem11b  38038  4atlem12b  38041  lneq2at  38208  cdlema1N  38221  cdlemblem  38223  paddss12  38249  paddasslem2  38251  paddasslem4  38253  paddasslem6  38255  paddasslem12  38261  paddunN  38357  poml4N  38383  poml5N  38384  osumcllem6N  38391  pexmidlem6N  38405  pl42lem2N  38410  ltrnu  38551  ltrneq2  38578  trlval2  38593  cdlemd6  38633  cdleme25b  38784  cdleme29b  38805  cdlemefr29exN  38832  ltrniotacnvval  39012  cdlemk28-3  39338  dochexmidlem7  39896  muldvds2d  40423  frlmsnic  40689  nna4b4nsq  40936  mzpsubmpt  41004  mzpsubst  41009  eqrabdioph  41038  rabdiophlem2  41063  elpell14qr2  41123  elpell1qr2  41133  pellfundre  41142  pellfundge  41143  pellfundglb  41146  pellfund14gap  41148  congabseq  41236  jm2.22  41257  jm2.23  41258  jm2.26lem3  41263  wepwsolem  41307  dnwech  41313  aomclem2  41320  aomclem4  41322  pwfi2f1o  41361  onexlimgt  41515  oaltublim  41563  oege1  41578  cantnfub2  41594  cantnfresb  41596  cantnf2  41597  oacl2g  41602  ss2iundf  41873  dssmapf1od  42235  neik0pk1imk0  42261  gneispace  42348  grur1cld  42454  cpcolld  42480  mnuop23d  42488  mnuprdlem1  42494  mnuprdlem2  42495  mnurndlem1  42503  grumnudlem  42507  radcnvrat  42536  sbiota1  42656  ordelordALT  42761  2pm13.193  42776  ee11an  42914  refsumcn  43177  rfcnnnub  43183  disjxp1  43219  xrnmnfpnf  43235  ssinc  43239  nssd  43257  disjf1o  43346  disjinfi  43348  choicefi  43357  axccdom  43379  dmrelrnrel  43383  monoords  43467  fperiodmullem  43473  xadd0ge  43490  xrssre  43518  xrlexaddrp  43522  xrred  43535  infxr  43537  xrnpnfmnf  43646  monoordxrv  43653  monoord2xrv  43655  fsumiunss  43748  fmul01  43753  fmuldfeqlem1  43755  fmuldfeq  43756  fmul01lt1lem1  43757  fmul01lt1lem2  43758  cncfmptss  43760  climinf  43779  climsuselem1  43780  climsuse  43781  limcperiod  43801  limcrecl  43802  sumnnodd  43803  limcleqr  43817  0ellimcdiv  43822  climleltrp  43849  limsuppnfdlem  43874  limsupresxr  43939  liminfresxr  43940  liminfvalxr  43956  cnrefiisplem  44002  xlimmnfvlem1  44005  xlimpnfvlem1  44009  cncfperiod  44052  icccncfext  44060  cncfiooicclem1  44066  dvbdfbdioolem1  44101  dvnmptdivc  44111  dvdsn1add  44112  dvnmptconst  44114  dvnmul  44116  dvmptfprodlem  44117  dvmptfprod  44118  dvnprodlem2  44120  iblspltprt  44146  itgsubsticclem  44148  itgspltprt  44152  itgsbtaddcnst  44155  stoweidlem3  44176  stoweidlem16  44189  stoweidlem17  44190  stoweidlem19  44192  stoweidlem20  44193  stoweidlem23  44196  stoweidlem25  44198  stoweidlem27  44200  stoweidlem31  44204  stoweidlem34  44207  stoweidlem42  44215  stoweidlem48  44221  stoweidlem51  44224  stoweidlem52  44225  stoweidlem59  44232  wallispilem1  44238  wallispilem3  44240  stirlinglem13  44259  fourierdlem16  44296  fourierdlem20  44300  fourierdlem21  44301  fourierdlem38  44318  fourierdlem42  44322  fourierdlem46  44325  fourierdlem48  44327  fourierdlem49  44328  fourierdlem50  44329  fourierdlem54  44333  fourierdlem68  44347  fourierdlem72  44351  fourierdlem73  44352  fourierdlem76  44355  fourierdlem79  44358  fourierdlem81  44360  fourierdlem86  44365  fourierdlem89  44368  fourierdlem90  44369  fourierdlem91  44370  fourierdlem92  44371  fourierdlem97  44376  fourierdlem101  44380  fourierdlem103  44382  fourierdlem104  44383  fourierdlem111  44390  etransclem24  44431  etransclem25  44432  etransclem28  44435  etransclem41  44448  etransclem44  44451  etransclem48  44455  salexct  44507  dfsalgen2  44514  sge0f1o  44555  sge0rnbnd  44566  sge0split  44582  sge0iunmptlemre  44588  sge0fodjrnlem  44589  sge0iunmpt  44591  nnfoctbdjlem  44628  iundjiunlem  44632  meadjiunlem  44638  ismeannd  44640  meaiuninclem  44653  omeiunle  44690  carageniuncllem1  44694  caratheodorylem1  44699  hoidmvlelem4  44771  hoiqssbllem2  44796  salpreimagelt  44880  salpreimalegt  44882  pimdecfgtioc  44888  smfaddlem2  44937  smflimlem6  44949  nsssmfmbflem  44951  smfpimcclem  44980  or2expropbilem1  45198  funressndmfvrn  45210  f1cof1b  45241  2leaddle2  45462  smonoord  45495  uniimaprimaeqfv  45506  fundcmpsurbijinjpreimafv  45531  fundcmpsurinjALT  45536  iccpartf  45555  ich2exprop  45595  ichnreuop  45596  ichreuopeq  45597  sprbisymrel  45623  fmtnodvds  45668  proththdlem  45737  gbowgt5  45886  gboge9  45888  gbege6  45889  stgoldbwt  45900  sbgoldbalt  45905  bgoldbnnsum3prm  45928  isomgrtrlem  45962  uspgrbisymrelALT  45989  ssnn0ssfz  46357  ldepspr  46486  seposep  46890  subthinc  46992  prsthinc  47006  iunord  47053  bnd2d  47058  setrecsss  47078
  Copyright terms: Public domain W3C validator