MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylbid Unicode version

Theorem sylbid 215
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylbid.1
sylbid.2
Assertion
Ref Expression
sylbid

Proof of Theorem sylbid
StepHypRef Expression
1 sylbid.1 . . 3
21biimpd 207 . 2
3 sylbid.2 . 2
42, 3syld 44 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  3imtr4d  268  ax12eq  2271  ax12el  2272  poltletr  5407  xp11  5447  xpcan  5448  xpcan2  5449  foconst  5811  fvmptdf  5967  elfvmptrab1  5976  suppssOLD  6020  fvn0fvelrn  6088  fmptsng  6092  fmptsnd  6093  fnprb  6129  fnprOLD  6130  soisores  6223  isomin  6233  weniso  6250  riotaxfrd  6288  eusvobj2  6289  oprabv  6345  ovmpt2df  6434  elovmpt2rab  6521  elovmpt2rab1  6522  nlimsucg  6677  bropopvvv  6880  f1o2ndf1  6908  suppss  6949  supp0cosupp0  6958  smoiso  7052  tz7.48lem  7125  oevn0  7184  oaass  7229  omword1  7241  omlimcl  7246  odi  7247  oneo  7249  omeulem1  7250  oewordi  7259  oeworde  7261  oelimcl  7268  oaabs2  7313  omabs  7315  nnneo  7319  dom2lem  7575  fundmen  7609  onfin  7728  domfi  7761  dif1enOLD  7772  dif1en  7773  isfinite2  7798  unfilem1  7804  elfiun  7910  dffi3  7911  supisoex  7953  ordiso2  7961  ordtypelem7  7970  brwdom3  8029  unxpwdom2  8035  noinfepOLD  8098  cantnflem1  8129  cantnf  8133  cantnflem1OLD  8152  cantnfOLD  8155  r1sdom  8213  r1ord3g  8218  rankr1ai  8237  rankonidlem  8267  bndrank  8280  rankunb  8289  tcrank  8323  wdomfil  8463  wdomnumr  8466  alephordi  8476  alephdom  8483  dfac3  8523  dfac12lem3  8546  cfeq0  8657  cfsmolem  8671  sornom  8678  fin23lem28  8741  fin23lem30  8743  isf32lem2  8755  fin1a2lem9  8809  axcc2lem  8837  axdc3lem2  8852  axdc4lem  8856  ttukeylem5  8914  alephreg  8978  pwcfsdom  8979  fpwwe2lem13  9041  fpwwe2  9042  pwfseqlem3  9059  gchina  9098  inatsk  9177  intgru  9213  grur1  9219  grutsk1  9220  addcanpi  9298  mulcanpi  9299  addnidpi  9300  ltexnq  9374  ltbtwnnq  9377  genpss  9403  genpcd  9405  genpnmax  9406  addclprlem1  9415  mulclprlem  9418  distrlem1pr  9424  distrlem4pr  9425  distrlem5pr  9426  ltexprlem3  9437  ltexprlem6  9440  ltexpri  9442  reclem4pr  9449  axpre-sup  9567  lelttr  9696  ltletr  9697  letr  9699  le2add  10059  ltleadd  10060  lt2sub  10075  le2sub  10076  mulge0  10095  prodgt0  10412  mulge0b  10437  squeeze0  10473  addltmul  10799  elnnz  10899  nn0lt2  10952  zextlt  10962  uzind2  10980  uzindOLD  10982  indstr  11179  nn01to3  11204  qreccl  11231  rpnnen1lem1  11237  rpnnen1lem2  11238  rpnnen1lem3  11239  rpnnen1lem5  11241  xrlelttr  11388  xrltletr  11389  xrletr  11390  xrrebnd  11398  qbtwnre  11427  qbtwnxr  11428  qextlt  11431  qextle  11432  xltnegi  11444  xmulasslem  11506  xlemul1a  11509  iccid  11603  icoshft  11671  prunioo  11678  difreicc  11681  iccsplit  11682  fzofzim  11869  elfznelfzo  11915  injresinjlem  11925  fleqceilz  11981  modirr  12057  om2uzf1oi  12064  fsuppmapnn0fiub0  12099  suppssfz  12100  seqf1olem1  12146  sqlecan  12274  facdiv  12365  facwordi  12367  faclbnd  12368  bcpasc  12399  hasheqf1oi  12424  hashdom  12447  hashgt12el  12481  hashgt12el2  12482  hashimarni  12497  seqcoll  12512  hash2pr  12515  hashtpg  12523  hashge3el3dif  12524  hash3tr  12529  fstwrdne  12580  elovmpt2wrd  12583  ccatrn  12606  ccatws1lenrev  12635  swrdeq  12671  swrdsymbeq  12672  swrdspsleq  12673  swrdswrd  12685  wrd2ind  12703  swrdccatin12lem2a  12710  swrdccat3  12717  swrdccat  12718  swrdccat3blem  12720  repswswrd  12756  cshwidxmod  12774  2cshw  12781  2cshwcshw  12793  scshwfzeqfzo  12794  cshwcsh2id  12796  swrd2lsw  12890  2swrd2eqwrdeq  12891  wwlktovf1  12895  sqrlem6  13081  resqrex  13084  absnid  13131  cau3lem  13187  sqreu  13193  rlim2lt  13320  rlim3  13321  o1lo1  13360  o1lo12  13361  rlimuni  13373  climuni  13375  lo1resb  13387  o1resb  13389  2clim  13395  o1rlimmul  13441  lo1le  13474  fsumss  13547  fsumabs  13615  cvgcmpce  13632  geomulcvg  13685  mertenslem2  13694  fprodss  13755  reeff1  13855  efieq1re  13934  dvdsmultr2  14021  dvdsleabs  14032  odd2np1lem  14045  odd2np1  14046  divalglem8  14058  sadcaddlem  14107  gcdneg  14164  gcddiv  14187  dvdssqim  14191  algcvga  14208  prmind2  14228  prmgt1  14236  prmn2uzge3  14237  coprmdvds  14243  coprmdvds2  14244  qredeq  14247  euclemma  14249  nprmdvds1  14252  prmdvdsexpr  14257  prmfac1  14259  divgcdodd  14260  crt  14308  eulerthlem2  14312  fermltl  14314  nnnn0modprm0  14331  coprimeprodsq2  14334  pythagtriplem2  14341  iserodd  14359  pcpremul  14367  pcdvdsb  14392  pc2dvds  14402  pc11  14403  pcfac  14418  prmpwdvds  14422  prmreclem4  14437  prmreclem5  14438  1arith  14445  4sqlem11  14473  vdwlem6  14504  vdwlem7  14505  vdwlem9  14507  vdwlem10  14508  vdwlem11  14509  ramub1lem2  14545  ramcl  14547  cshwshashlem3  14582  cshwrepswhash1  14587  prmlem0  14591  firest  14830  imasaddfnlem  14925  imasvscafn  14934  erlecpbl  14947  xpsff1o  14965  setcmon  15414  setcepi  15415  setciso  15418  pltnle  15596  pltletr  15601  plelttr  15602  joindmss  15637  joineu  15640  meetdmss  15651  meeteu  15654  psref  15838  dirge  15867  imasmnd2  15957  imasgrp2  16185  ghmpreima  16288  gaorber  16346  symgfvne  16413  idrespermg  16436  symgextf1  16446  gsmsymgrfixlem1  16452  gsmsymgrfix  16453  gsmsymgreqlem2  16456  symgfixelsi  16460  symgfixf1  16462  pmtrfrn  16483  symggen  16495  psgnunilem2  16520  psgnran  16540  mndodcongi  16567  sylow1lem1  16618  odcau  16624  sylow2alem1  16637  sylow2alem2  16638  lsmsubm  16673  lsmsubg  16674  lsmmod  16693  lsmdisj2  16700  efgtlen  16744  efgredlemc  16763  efgcpbllemb  16773  torsubg  16860  frgpnabllem1  16877  cyggexb  16901  gsumval3a  16905  gsumval3aOLD  16906  dprdsubg  17071  dprddisj2  17087  dprddisj2OLD  17088  dmdprdsplit2lem  17094  dmdprdsplit2  17095  ablfacrp  17117  ablfac1eulem  17123  pgpfac1lem3  17128  imasring  17268  unitgrp  17316  f1rhm0to0ALT  17390  mptscmfsupp0  17576  lmhmima  17693  lsmcl  17729  lsmelval2  17731  lspsneleq  17761  lpiss  17898  mplcoe5lem  18130  xrsdsreclb  18465  gzrngunitlem  18482  znidomb  18600  frgpcyg  18612  lindfrn  18856  f1lindf  18857  matecl  18927  mat1dimelbas  18973  mat1dimcrng  18979  dmatelnd  18998  dmatscmcl  19005  scmateALT  19014  scmatmulcl  19020  smatvscl  19026  scmatf1  19033  mat1scmat  19041  mdetdiaglem  19100  mdetunilem8  19121  cramer0  19192  mat2pmatf1  19230  pm2mpf1  19300  cayhamlem1  19367  cpmadugsumlemF  19377  cpmadumatpoly  19384  chcoeffeq  19387  tgtop  19475  neips  19614  neindisj  19618  restbas  19659  tgrest  19660  restcld  19673  restcldr  19675  ordtbas2  19692  ordtbas  19693  tgcn  19753  tgcnp  19754  subbascn  19755  cnconst2  19784  cnconst  19785  cnpresti  19789  cmpsublem  19899  tgcmp  19901  uncmp  19903  hauscmplem  19906  bwth  19910  bwthOLD  19911  conndisj  19917  nconsubb  19924  1stcfb  19946  2ndc1stc  19952  1stcrest  19954  2ndcctbss  19956  1stccnp  19963  llyrest  19986  nllyrest  19987  nllyidm  19990  cldllycmp  19996  1stckgen  20055  txcls  20105  txbasval  20107  txcnpi  20109  txcnp  20121  ptcnplem  20122  txdis1cn  20136  txlly  20137  txnlly  20138  pthaus  20139  tx1stc  20151  xkohaus  20154  xkococn  20161  basqtop  20212  qtopeu  20217  qtoprest  20218  qtopomap  20219  qtopcmap  20220  kqfvima  20231  kqsat  20232  kqcldsat  20234  fbfinnfr  20342  fgfil  20376  fgabs  20380  trfil2  20388  ufilmax  20408  isufil2  20409  ufprim  20410  ufileu  20420  filufint  20421  cfinufil  20429  elfm2  20449  rnelfmlem  20453  rnelfm  20454  fmfnfmlem2  20456  fmfnfmlem4  20458  fmfnfm  20459  ufldom  20463  flffbas  20496  flimfnfcls  20529  alexsublem  20544  alexsubALT  20551  symgtgp  20600  qustgpopn  20618  qustgplem  20619  tsmsxplem1  20655  bldisj  20901  xbln0  20917  blssps  20927  blss  20928  blin2  20932  blcls  21009  prdsxmslem2  21032  metustfbasOLD  21068  metustfbas  21069  xrsblre  21316  xrsmopn  21317  recld2  21319  reperflem  21323  reconnlem2  21332  cnmpt2pc  21428  cnheibor  21455  lebnumlem3  21463  nmhmcn  21603  cphsqrtcl2  21633  iscau3  21717  iscau4  21718  iscmet3lem2  21731  lmcau  21751  cmetss  21753  bcth3  21770  cmetcusp1OLD  21791  cmetcusp1  21792  minveclem3b  21843  ivthlem2  21864  ivthlem3  21865  ovolctb  21901  ovolscalem1  21924  ovolicc2lem3  21930  ovolicc2lem4  21931  dyaddisjlem  22004  dyadmbllem  22008  opnmbllem  22010  subopnmbl  22013  volivth  22016  mbfimaopn2  22064  i1faddlem  22100  i1fmullem  22101  itg10a  22117  itg1ge0a  22118  mbfi1fseqlem4  22125  mbfi1flimlem  22129  dveflem  22380  dvlip2  22396  dvne0  22412  lhop1lem  22414  lhop1  22415  lhop2  22416  lhop  22417  dvcvx  22421  dvfsumrlim  22432  ftc1lem6  22442  itgsubst  22450  coe1mul3  22500  dvdsq1p  22561  coemullem  22647  coe1termlem  22655  dgrco  22672  coecj  22675  aaliou3lem7  22745  ulmcn  22794  reeff1o  22842  sincosq3sgn  22893  sincosq4sgn  22894  sineq0  22914  recosf1o  22922  efopn  23039  cxpge0  23064  cxpcn3lem  23121  cxpeq  23131  angpieqvd  23162  atantayl2  23269  rlimcnp  23295  xrlimcnp  23298  cxploglim  23307  ftalem2  23347  muval1  23407  ppiublem1  23477  chtub  23487  dchrmulcl  23524  dchrsum2  23543  bclbnd  23555  bposlem1  23559  bposlem5  23563  lgsdirnn0  23614  lgsqrlem2  23617  lgseisenlem2  23625  lgsquadlem1  23629  2sqblem  23652  chtppilimlem2  23659  dchrisumlem3  23676  dchrisum0lem1  23701  pntlem3  23794  ostth2lem2  23819  ostth3  23823  brbtwn2  24208  colinearalg  24213  axbtwnid  24242  axlowdimlem14  24258  axlowdimlem15  24259  axcontlem2  24268  ushgrauhgra  24303  usgra0v  24371  usgraedgrn  24381  usgra2edg  24382  usgrarnedg  24384  usgra1v  24390  usgraidx2v  24393  usgrafisindb0  24408  usgrafisindb1  24409  nbgraisvtx  24431  nbgraf1olem1  24441  nbgraf1olem5  24445  nb3graprlem1  24451  cusgrarn  24459  cusgrasize2inds  24477  uvtxnbgra  24493  uvtxnb  24497  trliswlk  24541  pthdepisspth  24576  redwlk  24608  usgra2wlkspthlem1  24619  usgra2wlkspth  24621  cyclnspth  24631  fargshiftf1  24637  usgrcyclnl1  24640  usgrcyclnl2  24641  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv  24667  4cycl4dv4e  24668  wwlknimp  24687  wwlkn0  24689  wlkiswwlk1  24690  wlkiswwlk2  24697  wlklniswwlkn2  24700  wlknwwlkninj  24711  wlkiswwlkinj  24718  wwlknred  24723  wwlknextbi  24725  wwlkextinj  24730  wwlkm1edg  24735  wwlkextproplem3  24743  clwlkswlks  24758  clwwlkgt0  24771  clwwlknprop  24772  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwlkisclwwlk  24789  clwwlkf  24794  clwwlkf1  24796  clwwisshclwwlem  24806  clwwisshclww  24807  erclwwlkeqlen  24812  erclwwlksym  24814  erclwwlktr  24815  erclwwlkneqlen  24824  erclwwlknsym  24826  erclwwlkntr  24827  eleclclwwlkn  24833  hashecclwwlkn1  24834  usghashecclwwlk  24835  wlklenvclwlk  24839  clwlkfoclwwlk  24845  clwlkf1clwwlk  24850  el2wlkonot  24869  el2spthonot  24870  el2spthonot0  24871  2wlkonot3v  24875  2spthonot3v  24876  el2wlksotot  24882  usg2wlkonot  24883  usg2wotspth  24884  2spontn0vne  24887  usg2spthonot  24888  usg2spthonot0  24889  vdusgra0nedg  24908  nbhashuvtx1  24915  usgravd0nedg  24918  rusgrargra  24930  rusgrasn  24945  rusgranumwlklem1  24949  rusgranumwlks  24956  clwlknclwlkdifs  24960  3vfriswmgra  25005  1to2vfriswmgra  25006  2pthfrgra  25011  frgrancvvdeqlem2  25031  frgrawopreg1  25050  frgrawopreg2  25051  frg2wot1  25057  frg2woteqm  25059  frg2woteq  25060  2spotiundisj  25062  usg2spot2nb  25065  usgreg2spot  25067  2spotmdisj  25068  frgregordn0  25070  extwwlkfablem2  25078  numclwwlkovf2ex  25086  numclwwlkovgelim  25089  extwwlkfab  25090  numclwlk1lem2foa  25091  numclwlk1lem2f  25092  numclwlk1lem2f1  25094  numclwlk1lem2fo  25095  numclwwlk2lem1  25102  numclwlk2lem2f  25103  numclwlk2lem2f1o  25105  frgrareggt1  25116  frgrareg  25117  frgraregord013  25118  isabloda  25301  blocnilem  25719  ipasslem11  25755  h1de2ctlem  26473  spansneleq  26488  spansnss  26489  normcan  26494  spansncvi  26570  nmcexi  26945  elpjrn  27109  stadd3i  27167  cvcon3  27203  dmdbr5  27227  ssdmd2  27233  atom1d  27272  superpos  27273  cvexchlem  27287  atcv0eq  27298  atexch  27300  atcvat4i  27316  atdmd  27317  atmd2  27319  mdsymlem3  27324  mdsymlem5  27326  sumdmdlem  27337  cdjreui  27351  nn0sqeq1  27562  mul2lt0bi  27569  cnre2csqlem  27892  ballotlemfrceq  28467  erdszelem4  28638  erdszelem9  28643  sconpi1  28684  mrsubvrs  28882  mvhf1  28919  mclsppslem  28943  relexpsucl  29055  rtrclreclem.trans  29069  dvdspw  29175  predpo  29264  uzsinds  29296  omsinds  29299  soseq  29334  wsuclem  29381  sltres  29424  nodenselem3  29443  nodenselem4  29444  nodenselem5  29445  nodenselem8  29448  nofulllem5  29466  cgrid2  29653  cgrextend  29658  btwnswapid2  29668  btwnexch3  29670  btwnexch  29675  ifscgr  29694  btwnxfr  29706  colineardim1  29711  colinearxfr  29725  lineext  29726  fscgr  29730  brsegle2  29759  seglecgr12im  29760  seglecgr12  29761  segletr  29764  segleantisym  29765  colinbtwnle  29768  broutsideof2  29772  outsideofeq  29780  outsidele  29782  lineunray  29797  lineelsb2  29798  elhf2  29832  ordtopcon  29904  ordtopt0  29907  opnmbllem0  30050  mblfinlem3  30053  ovoliunnfl  30056  voliunnfl  30058  dvtanlem  30064  itg2addnclem  30066  itg2addnclem2  30067  itg2addnclem3  30068  itg2gt0cn  30070  ftc1cnnc  30089  ftc2nc  30099  areacirclem1  30107  areacirclem2  30108  areacirclem4  30110  areacirc  30112  nn0prpwlem  30140  nn0prpw  30141  cldbnd  30144  fgmin  30188  tailfb  30195  indexdom  30225  fzmul  30233  fzadd2  30234  sdclem2  30235  sdclem1  30236  fdc  30238  incsequz  30241  sstotbnd2  30270  equivbnd  30286  prdstotbnd  30290  grpokerinj  30347  keridl  30429  smprngopr  30449  ispridlc  30467  dmncan2  30474  diophin  30706  diophun  30707  fphpdo  30751  pellexlem1  30765  pell1234qrne0  30789  pell14qrgt0  30795  pell1234qrdich  30797  pell1qrge1  30806  elpell1qr2  30808  pell1qrgap  30810  pellfundex  30822  rmxypairf1o  30847  jm2.26a  30942  setindtr  30966  rpnnen3  30974  dnnumch3  30993  fnwe2lem2  30997  pwssplit4  31035  hbtlem5  31077  lcmneg  31209  nznngen  31221  zm1nn  32325  2elfz2melfz  32334  subsubelfzo0  32338  usgra2pthspth  32351  spthdifv  32352  usgra2pth  32354  ushguhg  32371  uhgrasiz  32394  usgedgvadf1  32415  usgedgvadf1ALT  32418  usgrafiedgALT  32451  isassintop  32534  mgm2mgm  32551  tpres  32554  ciclcl  32586  cicrcl  32587  cicsym  32588  cictr  32589  iszeroi  32615  initoeu2lem1  32620  initoeu2  32622  estrcbasbas  32637  funcestrcsetclem9  32654  fthestrcsetc  32656  fullestrcsetc  32657  equivestrcsetc  32658  embedsetcestrclem  32663  funcsetcestrclem9  32669  fthsetcestrc  32671  fullsetcestrc  32672  lidldomn1  32727  zlidlring  32734  uzlidlring  32735  rngcsect  32788  rngciso  32790  rngcisoOLD  32802  rhmsscrnghm  32834  rhmsubcrngclem1  32835  ringcsect  32839  ringciso  32841  ringcbasbas  32842  funcringcsetcOLD2lem9  32852  ringcisoOLD  32865  ringcbasbasOLD  32866  funcringcsetclem9OLD  32875  nzerooringczr  32880  ztprmneprm  32936  nn0sumltlt  32939  nn0le2is012  32956  scmsuppss  32965  ply1mulgsumlem1  32986  ply1mulgsumlem2  32987  lincsumcl  33032  lincscmcl  33033  ellcoellss  33036  lindslinindsimp1  33058  lindslinindimp2lem4  33062  lindslinindsimp2lem5  33063  lindslinindsimp2  33064  lindsrng01  33069  snlindsntor  33072  ldepspr  33074  lincresunit3  33082  islininds2  33085  isldepslvec2  33086  lmod1  33093  bj-bary1lem1  34680  lshpdisj  34712  lsat0cv  34758  lcvexchlem4  34762  lcvexchlem5  34763  lsatcv0eq  34772  lfl1dim  34846  lfl1dim2N  34847  lkrss2N  34894  lkreqN  34895  cmtbr3N  34979  omlfh3N  34984  cvrnbtwn  34996  cvrcon3b  35002  atnle  35042  cvlatexch1  35061  cvlsupr2  35068  hlrelat2  35127  cvrexchlem  35143  cvrat  35146  atcvr0eq  35150  atcvrj0  35152  atltcvr  35159  cvrat4  35167  lvolex3N  35262  islpln2a  35272  lplnriaN  35274  llncvrlpln2  35281  islvol2aN  35316  lplncvrlvol2  35339  dalem-cly  35395  dalem44  35440  snatpsubN  35474  pointpsubN  35475  lncvrelatN  35505  cdlemblem  35517  paddasslem16  35559  paddidm  35565  pmodlem2  35571  pmapjoin  35576  llnexchb2  35593  llnexch2N  35594  pclfinclN  35674  linepsubclN  35675  lhpj1  35746  lhp2atnle  35757  lautcvr  35816  trlnidatb  35902  trlnid  35904  cdleme32e  36171  erng1lem  36713  erngdvlem4-rN  36725  diaelrnN  36772  diaf11N  36776  dibf11N  36888  cdlemn11pre  36937  dihord2pre  36952  dihord6apre  36983  dihvalrel  37006  dihglblem5apreN  37018  dihmeetlem13N  37046  mapdordlem2  37364  baerlem3lem2  37437  baerlem5alem2  37438  baerlem5blem2  37439  mapdheq2  37456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator