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  2037  sb4  2057  sbft  2080  ax12indalem  2255  ax12inda2ALT  2256  gencl  3111  spsbc  3310  eqsbc3r  3359  ssnelpss  3856  uniintsn  4282  prex  4651  copsexg  4693  ordtri3  4872  posn  5024  optocl  5030  funimass1  5610  f1ocnvb  5776  eqfnfv2  5921  elpreima  5946  fconst5  6060  dff13  6096  f1ocnvfv  6110  f1ocnvfvb  6111  fliftfun  6136  eusvobj2  6215  sorpsscmpl  6504  ssonprc  6536  xpexr  6651  xpexcnv  6653  relcnvexb  6659  dmfex  6668  frxp  6816  mpt2xopn0yelv  6864  rntpos  6892  oawordeulem  7127  oalimcl  7133  odi  7152  omeulem2  7156  oeeulem  7174  erexb  7260  unxpdomlem2  7653  dif1enOLD  7679  dif1en  7680  enp1ilem  7681  findcard2  7687  isfinite2  7705  unfi  7714  fodomfib  7726  inf0  7964  rankxplim2  8224  scott0  8230  ficardom  8268  cardaleph  8396  dfac5  8435  cflim2  8569  fin23lem23  8632  fin23lem28  8646  isf32lem5  8663  domtriomlem  8748  ac6num  8785  zorn2lem5  8806  zorn2lem6  8807  iunfo  8840  axrepndlem2  8894  axregnd  8907  axregndOLD  8908  hargch  8977  addcanpi  9205  mulcanpi  9206  indpi  9213  ltaddnq  9280  ltexnq  9281  prlem934  9339  ltaddpr2  9341  ltaprlem  9350  supsrlem  9415  ssxr  9581  ltxrlt  9582  addcan  9690  addcan2  9691  neg11  9797  negreb  9811  mulcand  10106  receu  10118  lemul1a  10320  cju  10456  nn1suc  10481  nnaddcl  10482  nndivtr  10501  znegclb  10820  zmulcl  10831  zeo  10865  uz11  11022  uzp1  11033  eqreznegel  11079  rpnnen1  11123  xrltne  11276  xneg11  11324  xnegdi  11350  xrsupss  11410  xrinfmss  11411  elfznelfzob  11776  modadd1  11890  modmul1  11897  om2uzlti  11918  bccmpl  12242  hashen  12275  fz1eqb  12281  hashfn  12296  hashnn0n0nn  12311  hashtpg  12344  eqwrd  12423  ccatopth  12522  ccatopth2  12523  swrdccatin2  12536  swrdccat3a  12543  cj11  12809  rennim  12886  cnpart  12887  sqrmo  12899  sqrgt0  12906  sqreulem  13005  sqreu  13006  lo1o1  13168  lo1eq  13204  rlimeq  13205  sumss  13359  cvgcmp  13437  efne0  13539  dvdseq  13738  divalglem8  13762  bitsinv1lem  13795  pcfac  14119  prmreclem3  14137  sectmon  14875  yoniso  15254  lublecllem  15317  oduposb  15465  grpinveu  15731  mulgass  15816  galcan  15981  symg1bas  16060  cayleylem2  16077  odbezout  16220  odeq1  16222  dprddomcld  16658  dvreq1  16961  unitrrg  17541  coe1tm  17908  frgpcyg  18199  obslbs  18348  tgss3  18990  uptx  19597  txindislem  19605  qtopeu  19688  hmeocnvb  19746  qtophmeo  19789  trufil  19882  ufinffr  19901  ghmcnp  20084  tgioo  20772  lmmcvg  21171  bcth3  21241  ovolunlem1a  21378  vitali  21493  ismbf  21508  ismbfcn  21509  rolle  21862  itgsubstlem  21920  vieta1lem2  22177  elqaalem3  22187  aacjcl  22193  efif1olem4  22401  lognegb  22438  logcj  22455  argimgt0  22461  logdmnrp  22486  logcnlem3  22489  logrec  22615  dcubic  22641  isppw  22852  rplogsumlem2  23134  pntpbnd1  23235  axlowdimlem16  23672  is2wlk  23933  grpoinveu  24178  grpoinvf  24196  diporthcom  24583  norm1exi  25122  shmodsi  25261  shmodi  25262  dfch2  25279  orthin  25318  chssoc  25368  spansncvi  25524  kbpj  25829  lnopunilem1  25883  cnlnssadj  25953  bra11  25981  strlem4  26127  strlem5  26128  hstrlem4  26135  hstrlem5  26136  dmdmd  26173  mdslle1i  26190  mdslle2i  26191  mdslmd1lem1  26198  atcvatlem  26258  atcvat4i  26270  mdsymlem3  26278  bcm1n  26540  xmulcand  26557  xreceu  26558  tpr2rico  26799  fprodser  27918  funpsstri  28032  sltres  28261  nofulllem1  28299  nofulllem2  28300  btwnintr  28506  idinside  28571  btwnconn1lem13  28586  wl-equsal1i  28832  dvtanlem  28901  fneval  29019  ismtybndlem  29165  grpoeqdivid  29206  0rngo  29287  expgrowth  30069  sbiota1  30148  nbgrassvwo2  31154  usgra2pth  31178  wwlkn0  31200  wlkiswwlk1  31201  wlklniswwlkn1  31210  wlklniswwlkn2  31211  el2wlkonot  31265  wwlksubclwwlk  31343  frg2wot1  31527  bnj1125  32826  bj-sb4v  33117  bj-sbftv  33125  bj-equsal1t  33175  bj-ldiv  33445  bj-bary1lem1  33451  bj-bary1  33452  lcvexchlem4  33533  lcvexchlem5  33534  opcon3b  33692  2dim  33965  ps-1  33972  paddclN  34337  ltrnnid  34631  cdleme22b  34836  dihmeetlem13N  35815  dih1dimatlem  35825  dihlspsnat  35829
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