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

Theorem syl5ibcom 220
Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)
Hypotheses
Ref Expression
syl5ib.1
syl5ib.2
Assertion
Ref Expression
syl5ibcom

Proof of Theorem syl5ibcom
StepHypRef Expression
1 syl5ib.1 . . 3
2 syl5ib.2 . . 3
31, 2syl5ib 219 . 2
43com12 31 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  biimpcd  224  mob2  3279  rmob  3430  disjxun  4450  sotric  4831  sotrieq  4832  nordeq  4902  nsuceq0  4963  suctr  4966  iss  5326  poirr2  5396  xp11  5447  tz6.12c  5890  fnbrfvb  5913  foeqcnvco  6203  f1eqcocnv  6204  dfwe2  6617  mpt2sn  6891  tfrlem15  7080  tz7.44-2  7092  tz7.48-1  7127  tz7.49  7129  oawordexr  7224  oewordi  7259  oeeulem  7269  nna0r  7277  nnawordex  7305  nnaordex  7306  oaabs  7312  oaabs2  7313  ectocld  7397  ecoptocl  7420  mapsn  7480  eqeng  7569  difsnen  7619  fopwdom  7645  frfi  7785  elfiun  7910  ordiso  7962  ordtypelem7  7970  wemaplem2  7993  suc11reg  8057  inf3lem6  8071  noinfep  8097  cantnff  8114  cantnfp1lem2  8119  cantnfp1lem3  8120  cantnflem1  8129  cantnf  8133  cantnfp1lem2OLD  8145  cantnfp1lem3OLD  8146  cantnflem1OLD  8152  cantnfOLD  8155  r111  8214  rankc2  8310  tcrank  8323  cardnueq0  8366  fodomfi2  8462  alephinit  8497  dfac9  8537  dfac12k  8548  cdainf  8593  ackbij1  8639  ackbij2  8644  sornom  8678  fin23lem16  8736  fin23lem21  8740  isf32lem2  8755  fin1a2lem6  8806  itunitc  8822  zorn2lem4  8900  wunr1om  9118  tskr1om  9166  recmulnq  9363  ltexnq  9374  distrlem4pr  9425  1re  9616  0re  9617  0cnALT  9832  mulge0  10095  prodgt0  10412  peano2nn  10573  recnz  10963  zneo  10970  uzn0  11125  xlemul1a  11509  prunioo  11678  flidz  11947  ceilidz  11979  modid2  12023  om2uzrani  12063  uzrdgfni  12069  seqid  12152  seqz  12155  facdiv  12365  facwordi  12367  hashdom  12447  wrdnval  12571  wrdl1s1  12622  sqrmo  13085  fsumf1o  13545  isumltss  13660  supcvg  13667  dvdsnegb  14001  odd2np1lem  14045  odd2np1  14046  bitsuz  14124  bezoutlem4  14179  gcddiv  14187  gcdeq  14190  dvdssqim  14191  dvdsprm  14240  coprm  14241  coprmdvds2  14244  prmdvdsexp  14255  rpmul  14264  prmdiv  14315  opoe  14335  omoe  14336  opeo  14337  omeo  14338  pythagtriplem19  14357  pc2dvds  14402  pcadd  14408  prmpwdvds  14422  vdwlem11  14509  ramubcl  14536  0ram  14538  mreexexd  15045  posasymb  15582  pleval2  15595  pltval3  15597  plttr  15600  pospo  15603  letsr  15857  intopsn  15882  ismgmid  15891  imasmnd2  15957  isgrpid2  16086  isgrpinv  16100  imasgrp2  16185  orbsta  16351  symgfix2  16441  pmtrfrn  16483  pmtrrn2  16485  odmulg  16578  odmulgeq  16579  gexdvdsi  16603  gexnnod  16608  pgpssslw  16634  sylow2alem1  16637  fislw  16645  lsmss1b  16685  lsmss2b  16687  efgrelexlemb  16768  torsubg  16860  ablfacrplem  17116  pgpfac1lem2  17126  pgpfac1lem3  17128  imasring  17268  dvdsrcl2  17299  dvdsrtr  17301  dvdsrmul1  17302  irredn0  17352  lspsneq0  17658  lmhmima  17693  lspsolv  17789  opsrtoslem2  18149  mpfind  18205  mpfpf1  18387  pf1mpf  18388  xrsdsreclblem  18464  dvdsrzring  18507  dvdsrz  18508  prmirredlem  18523  prmirredlemOLD  18526  znunit  18602  pjdm2  18742  obselocv  18759  lindfrn  18856  cpmadugsumlemF  19377  baspartn  19455  bastop  19483  iscld3  19565  isopn3  19567  iscldtop  19596  ordtrest2lem  19704  2ndcredom  19951  2ndc1stc  19952  2ndcrest  19955  2ndcdisj  19957  2ndcsep  19960  kgenidm  20048  dfac14  20119  tx2ndc  20152  kqreglem1  20242  rnelfm  20454  fmfnfmlem2  20456  fmfnfmlem4  20458  fmfnfm  20459  flimtopon  20471  fclstopon  20513  xrsmopn  21317  icccmplem2  21328  reconnlem1  21331  iccpnfcnv  21444  cphsqrtcl2  21633  ivthlem3  21865  ivthicc  21870  ovolctb  21901  ioombl  21975  itgabs  22241  itgsplitioo  22244  dvlip  22394  c1liplem1  22397  c1lip1  22398  dvgt0lem1  22403  dvivthlem2  22410  dvne0  22412  lhop1lem  22414  lhop1  22415  lhop2  22416  lhop  22417  dvcvx  22421  itgsubstlem  22449  mdegnn0cl  22471  ig1peu  22572  elply2  22593  plypf1  22609  dgreq0  22662  aannenlem3  22726  abelthlem2  22827  lognegb  22974  eflogeq  22986  efopn  23039  cxpge0  23064  cxplea  23077  cxple2  23078  cxpcn3lem  23121  cxpaddlelem  23125  cxpaddle  23126  cxpeq  23131  asinsinb  23228  acoscosb  23229  atantanb  23255  leibpilem1  23271  wilthlem2  23343  sqf11  23413  sqff1o  23456  ppiublem1  23477  lgsdir  23605  lgsne0  23608  lgsquadlem3  23631  2sqblem  23652  dchrisum0flblem1  23693  ostth3  23823  ostth  23824  colinearalg  24213  axcontlem5  24271  axcontlem9  24275  umgraf  24318  uslgraf1oedg  24359  nbgrassvwo  24437  usgrcyclnl1  24640  nvnencycllem  24643  clwwlknprop  24772  clwlkf1clwwlklem1  24846  usg2wlkonot  24883  usg2wotspth  24884  eupath2lem2  24978  eupath2lem3  24979  isgrp2d  25237  rngosn3  25428  htthlem  25834  pjpreeq  26316  h1dn0  26470  spansneleqi  26487  rnbra  27026  dfpjop  27101  elpjrn  27109  stm1i  27162  mdbr2  27215  mdsl2i  27241  sumdmdlem  27337  dmdbr6ati  27342  ordtrest2NEWlem  27904  xrge0iifcnv  27915  eulerpartlemb  28307  erdszelem8  28642  cvmlift3lem4  28767  cvmlift3lem5  28768  mrsub0  28876  mrsubccat  28878  mrsubcn  28879  msubrn  28889  msrid  28905  elmthm  28936  ghomgrpilem2  29026  dvdspw  29175  dfon2lem9  29223  poseq  29333  nodenselem3  29443  nodenselem5  29445  nodenselem8  29448  nofulllem5  29466  btwnconn1lem11  29747  broutsideof2  29772  fin2so  30040  itgabsnc  30084  ftc2nc  30099  opnbnd  30143  tailfb  30195  sdclem2  30235  subspopn  30245  equivtotbnd  30274  igenval2  30463  isfldidl  30465  ismrc  30633  pellexlem1  30765  aomclem4  31003  dfac21  31012  lsmfgcl  31020  lmhmfgima  31030  dfacbasgrp  31057  hbtlem6  31078  fiuneneq  31154  lcmgcdeq  31216  stoweidlem27  31809  stoweidlem29  31811  assintopass  32538  lshpinN  34714  lsatcv0eq  34772  lsatcv1  34773  cvrnbtwn3  35001  cvrnbtwn4  35004  cvrcmp  35008  atnlt  35038  cvlexchb1  35055  2llnne2N  35132  atcvr0eq  35150  lnnat  35151  cvrat4  35167  ps-1  35201  3at  35214  llncmp  35246  llnnlt  35247  llncvrlpln2  35281  llncvrlpln  35282  lplncmp  35286  lplnnlt  35289  lplncvrlvol2  35339  lplncvrlvol  35340  lvolcmp  35341  lvolnltN  35342  dalempnes  35375  dalemqnet  35376  dalem-cly  35395  dalem44  35440  lncmp  35507  cdlemblem  35517  llnexch2N  35594  osumcllem4N  35683  pexmidlem1N  35694  lhp2atnle  35757  cdleme11dN  35987  cdleme20k  36045  cdleme21at  36054  cdleme21ct  36055  cdleme32e  36171  cdleme35f  36180  tendoex  36701  dochexmidlem1  37187  lcfrlem9  37277  mapd1o  37375  mapdindp3  37449
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