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

Theorem syl6bi 228
Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)
Hypotheses
Ref Expression
syl6bi.1
syl6bi.2
Assertion
Ref Expression
syl6bi

Proof of Theorem syl6bi
StepHypRef Expression
1 syl6bi.1 . . 3
21biimpd 207 . 2
3 syl6bi.2 . 2
42, 3syl6 33 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  ax12i  1738  sb3  2096  2eu2  2378  rgen2aOLD  2885  reu6  3288  sseq0  3817  disjel  3873  disjpss  3877  uneqdifeq  3916  preq12b  4206  prel12  4207  prneimg  4211  elinti  4295  zfrepclf  4569  dtru  4643  opth1g  4728  otsndisj  4757  otiunsndisj  4758  ordtr2  4927  nsuceq0  4963  ordssun  4982  ordequn  4983  elreldm  5232  issref  5385  relcnvtr  5532  relresfld  5539  funopg  5625  funimass2  5667  f0dom0  5774  fveqdmss  6026  eldmrexrnb  6038  fvcofneq  6039  fconstfvOLD  6134  elunirn  6163  oprabid  6323  limuni3  6687  peano5  6723  op1steq  6842  bropopvvv  6880  f1o2ndf1  6908  frxp  6910  fnwelem  6915  suppimacnv  6929  fvn0elsuppb  6936  suppfnss  6944  reldmtpos  6982  rntpos  6987  seqomlem2  7135  oaordi  7214  oa00  7227  oalimcl  7228  omeulem1  7250  nnaordi  7286  ecopovtrn  7433  undifixp  7525  mapdom2  7708  unxpdomlem3  7746  enp1i  7775  findcard2  7780  infssuni  7831  wdompwdom  8025  opthreg  8056  inf3lemd  8065  inf3lem2  8067  inf3lem6  8071  cnfcomlem  8164  cnfcom3  8169  karden  8334  carden2a  8368  alephdom  8483  dfac5lem4  8528  dfac12r  8547  kmlem2  8552  kmlem12  8562  cfslb2n  8669  alephsing  8677  fin23lem30  8743  fin1a2lem6  8806  fin1a2lem13  8813  axcc2lem  8837  domtriomlem  8843  axdc3lem2  8852  axdc4lem  8856  brdom6disj  8931  alephexp1  8975  pwfseq  9063  addnidpi  9300  indpi  9306  nqereu  9328  ltsonq  9368  distrlem5pr  9426  addcanpr  9445  suplem1pr  9451  suplem2pr  9452  ltsrpr  9475  ltsosr  9492  sqgt0sr  9504  leltne  9695  ltnsym  9704  ltlen  9707  eqlei  9715  eqlei2  9716  infm3  10527  nnunb  10816  0mnnnnn0  10853  elnnnn0b  10865  nn0ge2m1nn  10886  btwnz  10991  uz11  11132  zq  11217  xrleltne  11380  xltnegi  11444  xmulasslem2  11503  iccleub  11609  uznfz  11790  2ffzeq  11823  elfzonlteqm1  11891  elfznelfzob  11916  injresinjlem  11925  injresinj  11926  fleqceilz  11981  modadd1  12033  modmul1  12040  modirr  12057  uzrdgfni  12069  fsuppmapnn0fiub0  12099  fsuppmapnn0ub  12101  seqf1o  12148  hashrabsn01  12441  hashrabsn1  12442  hash1snb  12479  hashf1lem2  12505  hash2prde  12516  hash2pwpr  12519  hashge2el2dif  12521  hash2sspr  12526  ffz0iswrd  12568  lswlgt0cl  12590  ccatw2s1p1  12640  swrdvalodm2  12664  2swrd1eqwrdeq  12679  wrdind  12702  wrd2ind  12703  swrdccatin1  12708  swrdccat3blem  12720  2cshwcshw  12793  cshwcsh2id  12796  wrd2pr2op  12885  2swrd2eqwrdeq  12891  wwlktovf  12894  wwlktovfo  12896  rexico  13186  lo1le  13474  fsum2dlem  13585  ntrivcvg  13706  fprodss  13755  fprod2dlem  13784  0dvds  14004  gcdneg  14164  algcvga  14208  eucalglt  14214  opoe  14335  omoe  14336  opeo  14337  omeo  14338  pockthi  14425  prmreclem5  14438  ramtcl2  14529  cshwrepswhash1  14587  f1ocpbl  14922  f1ovscpbl  14923  f1olecpbl  14924  monhom  15130  epihom  15137  setciso  15418  ipopos  15790  gsumval2a  15906  ismnddef  15922  symg2bas  16423  symgfix2  16441  gsmsymgreq  16457  pmtrdifellem4  16504  mndodcongi  16567  pj1eu  16714  dprd2da  17091  rimf1o  17383  rimrhm  17384  brric2  17394  lspdisjb  17772  lspsnsubn0  17786  0ring01eq  17919  psrbaglefi  18023  psrbaglefiOLD  18024  obs2ss  18760  mamufacex  18891  mat0dim0  18969  mat0dimid  18970  mat0dimscm  18971  dmatmat  18996  scmatmat  19011  mat1scmat  19041  1mavmul  19050  mavmulsolcl  19053  gsummatr01  19161  cpmatpmat  19211  cpmadugsumlemF  19377  tg2  19466  unitgOLD  19469  tgcl  19471  neii1  19607  neii2  19609  neindisj2  19624  perfopn  19686  ordtbas2  19692  pnfnei  19721  mnfnei  19722  bwthOLD  19911  llyidm  19989  txlm  20149  qtopuni  20203  tgqtop  20213  isfild  20359  snfil  20365  fbunfip  20370  fgss2  20375  fmco  20462  fbflim2  20478  cnpflf2  20501  fcfelbas  20537  fcfneii  20538  alexsubALTlem2  20548  alexsubALT  20551  tgpconcompeqg  20610  tsmscl  20633  tgioo  21301  xrsmopn  21317  iccntr  21326  reconnlem2  21332  addcnlem  21368  htpycn  21473  phtpyhtpy  21482  pi1blem  21539  fgcfil  21710  ioombl1lem4  21971  dyadmbl  22009  itg2gt0  22167  ditgneg  22261  dvivthlem1  22409  coeeq2  22639  aannenlem2  22725  sineq0  22914  efif1o  22933  leibpilem1  23271  xrlimcnp  23298  vmacl  23392  efvmacl  23394  vmalelog  23480  dchrelbasd  23514  lgsqr  23621  uhgra0v  24310  umisuhgra  24327  uslisushgra  24363  uslisumgra  24364  usisuslgra  24365  usgra0v  24371  usgraedgprv  24376  usgra2edg  24382  usgrarnedg  24384  usgraedg4  24387  usgra1v  24390  usgrafisindb0  24408  usgrafisindb1  24409  nbgra0nb  24429  nbcusgra  24463  cusgrasize2inds  24477  cusgrafilem2  24480  usgrasscusgra  24483  uvtxisvtx  24490  2mwlk  24521  wlkcpr  24529  edgwlk  24531  usgrnloop  24565  pthistrl  24574  spthonepeq  24589  wlkdvspthlem  24609  usgra2adedgspthlem2  24612  usgra2adedgwlkonALT  24616  usgra2wlkspthlem1  24619  usgra2wlkspthlem2  24620  usgra2wlkspth  24621  crctistrl  24628  cyclispth  24629  cyclispthon  24633  fargshiftf  24636  fargshiftfo  24638  usgrcyclnl2  24641  3v3e3cycl1  24644  constr3trllem2  24651  4cycl4v4e  24666  4cycl4dv  24667  4cycl4dv4e  24668  wwlknimp  24687  wwlkiswwlkn  24702  2wlkeq  24707  usg2wlkeq  24708  wwlkextproplem3  24743  wwlkextprop  24744  clwwlkprop  24770  clwwlkgt0  24771  clwwlknprop  24772  clwwlknimp  24776  clwlkisclwwlklem2fv2  24783  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem1  24787  clwwlkisclwwlkn  24791  clwwlkext2edg  24802  hashecclwwlkn1  24834  usghashecclwwlk  24835  el2wlkonotlem  24862  el2wlkonot  24869  el2wlkonotot0  24872  2wlkonot3v  24875  2spthonot3v  24876  el2wlksotot  24882  usg2wlkonot  24883  2spontn0vne  24887  vdgr1a  24906  hashnbgravdg  24913  0eusgraiff0rgracl  24941  rusgrasn  24945  rusgra0edg  24955  clwlknclwlkdifs  24960  frgra3vlem2  25001  1to2vfriswmgra  25006  1to3vfriswmgra  25007  vdfrgra0  25022  vdn0frgrav2  25023  vdgn0frgrav2  25024  frgrancvvdeqlem2  25031  frgrancvvdeqlem4  25033  frgrancvvdeqlemC  25039  usgreghash2spotv  25066  frgregordn0  25070  numclwwlkovf2ex  25086  numclwlk1lem2f1  25094  frgrareggt1  25116  frgrareg  25117  frgraregord013  25118  frgraregord13  25119  clmgmOLD  25323  smgrpmgm  25337  smgrpassOLD  25338  dvrunz  25435  nmlno0lem  25708  normgt0  26044  ocin  26214  nmlnop0iALT  26914  nmopun  26933  cvpss  27204  cvnbtwn  27205  atcvati  27305  mdsymlem6  27327  ifbieq12d2  27420  issgon  28123  mbfmcnt  28239  ballotlemfc0  28431  ballotlemfcc  28432  mthmblem  28940  relexpindlem  29062  dfres3  29188  sltsgn1  29421  sltsgn2  29422  sltintdifex  29423  sltres  29424  pprodss4v  29534  funpartfun  29593  funpartfv  29595  5segofs  29656  btwnxfr  29706  brofs2  29727  brifs2  29728  btwnconn1  29751  segleantisym  29765  broutsideof2  29772  outsidene1  29773  outsidene2  29774  funray  29790  lineunray  29797  volsupnfl  30059  itg2addnclem  30066  cldbnd  30144  cover2  30204  sdclem2  30235  fdc  30238  sstotbnd3  30272  heibor1  30306  0rngo  30424  pw2f1ocnv  30979  iocinico  31179  expgrowthi  31238  iotavalsb  31340  ioogtlb  31528  iocgtlb  31535  iocleub  31536  icogelb  31542  icoltub  31545  iooltub  31548  stoweidlem31  31813  2reu2  32192  eu2ndop1stv  32207  funressnfv  32213  afvelrnb0  32249  otiunsndisjX  32301  2f1fvneq  32307  fzoopth  32340  2ffzoeq  32341  spthdifv  32352  uhg0v  32377  usgvincvad  32404  usgvincvadALT  32407  usgo0s0  32435  usgo0s0ALT  32436  usgo1s0ALT  32437  usgo1s0  32442  usgfis  32446  usgfisALT  32450  mgmpropd  32463  clcllaw  32515  intop  32527  assintop  32533  assintopcllaw  32536  inveq  32565  invcoisoid  32576  isocoinvid  32577  ciclcl  32586  cicrcl  32587  isinitoi  32609  istermoi  32610  2initoinv  32616  2termoinv  32623  embedsetcestrclem  32663  rngimf1o  32711  rngimrnghm  32712  c0snmgmhm  32720  elrngchom  32776  rnghmsubcsetclem1  32783  rnghmsubcsetclem2  32784  rngcid  32787  rngcinv  32789  rngciso  32790  elrngchomOLD  32794  rngccatidOLD  32797  rngcinvOLD  32801  rngcisoOLD  32802  funcrngcsetcALT  32807  zrinitorngc  32808  zrtermorngc  32809  elringchom  32822  rhmsubcsetclem1  32829  rhmsubcsetclem2  32830  ringcid  32833  rhmsubcrngclem1  32835  rhmsubcrngclem2  32836  ringcinv  32840  ringciso  32841  funcringcsetcOLD2lem7  32850  elringchomOLD  32857  ringccatidOLD  32860  ringcinvOLD  32864  ringcisoOLD  32865  funcringcsetclem7OLD  32873  irinitoringc  32877  zrtermoringc  32878  rhmsubclem3  32896  rhmsubclem4  32897  rhmsubcOLDlem3  32915  rhmsubcOLDlem4  32916  ztprmneprm  32936  nn0le2is012  32956  suppmptcfin  32972  linccl  33015  linc1  33026  lincolss  33035  ldepspr  33074  bi23imp1  33264  bj-ax12i  34226  bj-sb3v  34336  bj-dtru  34383  lsatcvat  34775  lshpkrex  34843  cmtbr3N  34979  atn0  35033  atnle  35042  cvlsupr4  35070  cvlsupr5  35071  cvlsupr6  35072  cvrval4N  35138  cvratlem  35145  2llnjN  35291  2lplnj  35344  linepsubN  35476  elpaddatiN  35529  elpcliN  35617  pclcmpatN  35625  ldilval  35837  ltrnu  35845  cdleme18d  36020  tendotp  36487  tendof  36489  tendovalco  36491  diatrl  36771  diaintclN  36785  dvheveccl  36839  dibintclN  36894  dihord6apre  36983  dihmeetlem1N  37017  dihpN  37063  dihintcl  37071  dochkrshp4  37116
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