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

Theorem syl5ib 219
Description: A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.)
Hypotheses
Ref Expression
syl5ib.1
syl5ib.2
Assertion
Ref Expression
syl5ib

Proof of Theorem syl5ib
StepHypRef Expression
1 syl5ib.1 . 2
2 syl5ib.2 . . 3
32biimpd 207 . 2
41, 3syl5 32 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  syl5ibcom  220  syl5ibr  221  dvelimdf  2077  sb4  2097  sbft  2120  ax12indalem  2275  ax12inda2ALT  2276  gencl  3139  spsbc  3340  eqsbc3r  3389  ssnelpss  3890  uniintsn  4324  prex  4694  copsexg  4737  ordtri3  4919  posn  5073  optocl  5081  funimass1  5666  f1ocnvb  5834  eqfnfv2  5982  elpreima  6007  fconst5  6128  dff13  6166  f1ocnvfv  6184  f1ocnvfvb  6185  fliftfun  6210  eusvobj2  6289  sorpsscmpl  6591  ssonprc  6627  xpexr  6740  xpexcnv  6742  relcnvexb  6748  dmfex  6758  frxp  6910  mpt2xopn0yelv  6960  rntpos  6987  oawordeulem  7222  oalimcl  7228  odi  7247  omeulem2  7251  oeeulem  7269  erexb  7355  unxpdomlem2  7745  dif1enOLD  7772  dif1en  7773  enp1ilem  7774  findcard2  7780  isfinite2  7798  unfi  7807  fodomfib  7820  inf0  8059  rankxplim2  8319  scott0  8325  ficardom  8363  cardaleph  8491  dfac5  8530  cflim2  8664  fin23lem23  8727  fin23lem28  8741  isf32lem5  8758  domtriomlem  8843  ac6num  8880  zorn2lem5  8901  zorn2lem6  8902  iunfo  8935  axrepndlem2  8989  axregnd  9002  axregndOLD  9003  hargch  9072  addcanpi  9298  mulcanpi  9299  indpi  9306  ltaddnq  9373  ltexnq  9374  prlem934  9432  ltaddpr2  9434  ltaprlem  9443  supsrlem  9509  ssxr  9675  ltxrlt  9676  addcan  9785  addcan2  9786  neg11  9893  negreb  9907  mulcand  10207  receu  10219  lemul1a  10421  cju  10557  nn1suc  10582  nnaddcl  10583  nndivtr  10602  znegclb  10926  zmulcl  10937  zeo  10973  uz11  11132  uzp1  11143  eqreznegel  11196  rpnnen1  11242  xrltne  11395  xneg11  11443  xnegdi  11469  xrsupss  11529  xrinfmss  11530  elfznelfzob  11916  modadd1  12033  modmul1  12040  om2uzlti  12061  bccmpl  12387  hashen  12420  fz1eqb  12426  hashfn  12443  hashnn0n0nn  12458  hashtpg  12523  eqwrd  12582  ccatopth  12695  ccatopth2  12696  swrdccatin2  12712  swrdccat3a  12719  cj11  12995  rennim  13072  cnpart  13073  sqrmo  13085  sqrtgt0  13092  sqreulem  13192  sqreu  13193  lo1o1  13355  lo1eq  13391  rlimeq  13392  sumss  13546  cvgcmp  13630  fprodser  13756  efne0  13832  dvdseq  14033  divalglem8  14058  bitsinv1lem  14091  pcfac  14418  prmreclem3  14436  sectmon  15172  yoniso  15554  lublecllem  15618  oduposb  15766  mgmb1mgm1  15883  sgrp2rid2  16044  grpinveu  16084  mulgass  16172  galcan  16342  symg1bas  16421  cayleylem2  16438  odbezout  16580  odeq1  16582  dprddomcld  17032  dvreq1  17342  unitrrg  17942  coe1tm  18314  frgpcyg  18612  obslbs  18761  tgss3  19488  uptx  20126  txindislem  20134  qtopeu  20217  hmeocnvb  20275  qtophmeo  20318  trufil  20411  ufinffr  20430  ghmcnp  20613  tgioo  21301  lmmcvg  21700  bcth3  21770  ovolunlem1a  21907  vitali  22022  ismbf  22037  ismbfcn  22038  rolle  22391  itgsubstlem  22449  vieta1lem2  22707  elqaalem3  22717  aacjcl  22723  efif1olem4  22932  lognegb  22974  logcj  22991  argimgt0  22997  logdmnrp  23022  logcnlem3  23025  logrec  23151  dcubic  23177  isppw  23388  rplogsumlem2  23670  pntpbnd1  23771  axlowdimlem16  24260  nbgrassvwo2  24438  is2wlk  24567  wwlkn0  24689  wlkiswwlk1  24690  wlklniswwlkn1  24699  wlklniswwlkn2  24700  wwlksubclwwlk  24804  el2wlkonot  24869  frg2wot1  25057  grpoinveu  25224  grpoinvf  25242  diporthcom  25629  norm1exi  26168  shmodsi  26307  shmodi  26308  dfch2  26325  orthin  26364  chssoc  26414  spansncvi  26570  kbpj  26875  lnopunilem1  26929  cnlnssadj  26999  bra11  27027  strlem4  27173  strlem5  27174  hstrlem4  27181  hstrlem5  27182  dmdmd  27219  mdslle1i  27236  mdslle2i  27237  mdslmd1lem1  27244  atcvatlem  27304  atcvat4i  27316  mdsymlem3  27324  bcm1n  27600  xmulcand  27617  xreceu  27618  tpr2rico  27894  mrsubff1  28874  mvhf1  28919  funpsstri  29195  sltres  29424  nofulllem1  29462  nofulllem2  29463  btwnintr  29669  idinside  29734  btwnconn1lem13  29749  wl-equsal1i  29996  dvtanlem  30064  fneval  30170  ismtybndlem  30302  grpoeqdivid  30343  0rngo  30424  nzss  31222  expgrowth  31240  sbiota1  31341  usgra2pth  32354  aacllem  33216  bnj1125  34048  bj-sb4v  34337  bj-sbftv  34345  bj-equsal1t  34395  bj-ldiv  34674  bj-bary1lem1  34680  bj-bary1  34681  lcvexchlem4  34762  lcvexchlem5  34763  opcon3b  34921  2dim  35194  ps-1  35201  paddclN  35566  ltrnnid  35860  cdleme22b  36067  dihmeetlem13N  37046  dih1dimatlem  37056  dihlspsnat  37060  frege58c  37948
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