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

Theorem syl5ib 213
Description: A mixed syllogism inference. (Contributed by NM, 5-Aug-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 201 . 2
41, 3syl5 31 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178
This theorem is referenced by:  syl5ibcom  214  syl5ibr  215  dvelimdf  2018  sb4  2038  sbft  2059  ax12indalem  2237  ax12inda2ALT  2238  gencl  2980  spsbc  3176  eqsbc3r  3225  ssnelpss  3719  uniintsn  4140  prex  4506  ordtri3  4726  posn  4878  optocl  4884  funimass1  5461  f1ocnvb  5624  eqfnfv2  5768  elpreima  5793  fconst5  5904  dff13  5939  f1ocnvfv  5953  f1ocnvfvb  5954  fliftfun  5973  eusvobj2  6053  sorpsscmpl  6341  ssonprc  6373  xpexr  6488  xpexcnv  6490  relcnvexb  6496  dmfex  6504  frxp  6651  mpt2xopn0yelv  6692  rntpos  6720  oawordeulem  6954  oalimcl  6960  odi  6979  omeulem2  6983  oeeulem  7001  erexb  7087  unxpdomlem2  7477  dif1enOLD  7503  dif1en  7504  enp1ilem  7505  findcard2  7511  isfinite2  7529  unfi  7538  fodomfib  7550  inf0  7774  rankxplim2  8034  scott0  8040  ficardom  8078  cardaleph  8206  dfac5  8245  cflim2  8379  fin23lem23  8442  fin23lem28  8456  isf32lem5  8473  domtriomlem  8558  ac6num  8595  zorn2lem5  8616  zorn2lem6  8617  iunfo  8650  axrepndlem2  8704  axregnd  8717  hargch  8786  addcanpi  9014  mulcanpi  9015  indpi  9022  ltaddnq  9089  ltexnq  9090  prlem934  9148  ltaddpr2  9150  ltaprlem  9159  supsrlem  9224  ssxr  9390  ltxrlt  9391  addcan  9499  addcan2  9500  neg11  9606  negreb  9620  mulcand  9915  receu  9927  lemul1a  10129  cju  10264  nn1suc  10289  nnaddcl  10290  nndivtr  10309  znegclb  10627  zmulcl  10638  zeo  10672  uz11  10828  uzp1  10839  eqreznegel  10885  rpnnen1  10929  xrltne  11082  xneg11  11130  xnegdi  11156  xrsupss  11216  xrinfmss  11217  elfznelfzob  11572  modadd1  11686  modmul1  11693  om2uzlti  11714  bccmpl  12026  hashen  12059  fz1eqb  12065  hashfn  12079  hashnn0n0nn  12094  hashtpg  12127  eqwrd  12206  ccatopth  12305  ccatopth2  12306  swrdccatin2  12319  swrdccat3a  12326  cj11  12592  rennim  12669  cnpart  12670  sqrmo  12682  sqrgt0  12689  sqreulem  12788  sqreu  12789  lo1o1  12951  lo1eq  12987  rlimeq  12988  sumss  13142  cvgcmp  13219  efne0  13321  dvdseq  13520  divalglem8  13544  bitsinv1lem  13577  pcfac  13901  prmreclem3  13919  sectmon  14656  yoniso  15035  lublecllem  15098  oduposb  15246  grpinveu  15509  mulgass  15594  galcan  15759  symg1bas  15838  cayleylem2  15855  odbezout  15996  odeq1  15998  dvreq1  16608  unitrrg  17173  coe1tm  17490  frgpcyg  17714  obslbs  17863  tgss3  18295  uptx  18902  txindislem  18910  qtopeu  18993  hmeocnvb  19051  qtophmeo  19094  trufil  19187  ufinffr  19206  ghmcnp  19389  tgioo  20073  lmmcvg  20472  bcth3  20542  ovolunlem1a  20679  vitali  20793  ismbf  20808  ismbfcn  20809  rolle  21162  itgsubstlem  21220  vieta1lem2  21518  elqaalem3  21528  aacjcl  21534  efif1olem4  21742  lognegb  21779  logcj  21796  argimgt0  21802  logdmnrp  21827  logcnlem3  21830  logrec  21956  dcubic  21982  isppw  22193  rplogsumlem2  22475  pntpbnd1  22576  axlowdimlem16  22882  is2wlk  23143  grpoinveu  23388  grpoinvf  23406  diporthcom  23793  norm1exi  24332  shmodsi  24471  shmodi  24472  dfch2  24489  orthin  24528  chssoc  24578  spansncvi  24734  kbpj  25039  lnopunilem1  25093  cnlnssadj  25163  bra11  25191  strlem4  25337  strlem5  25338  hstrlem4  25345  hstrlem5  25346  dmdmd  25383  mdslle1i  25400  mdslle2i  25401  mdslmd1lem1  25408  atcvatlem  25468  atcvat4i  25480  mdsymlem3  25488  bcm1n  25757  xmulcand  25774  xreceu  25775  tpr2rico  26051  fprodser  27164  funpsstri  27278  sltres  27507  nofulllem1  27545  nofulllem2  27546  btwnintr  27752  idinside  27817  btwnconn1lem13  27832  wl-equsal1t  28063  wl-equsal1i  28065  dvtanlem  28112  fneval  28230  ismtybndlem  28376  grpoeqdivid  28417  0rngo  28498  expgrowth  29282  sbiota1  29361  nbgrassvwo2  29951  usgra2pth  29975  wwlkn0  29997  wlkiswwlk1  29998  wlklniswwlkn1  30007  wlklniswwlkn2  30008  el2wlkonot  30062  wwlksubclwwlk  30140  frg2wot1  30324  bnj1125  31561  bj-sb4v  31777  bj-sbftv  31782  bj-equsal1t  31818  bj-ldiv  32033  bj-bary1lem1  32039  bj-bary1  32040  lcvexchlem4  32119  lcvexchlem5  32120  opcon3b  32278  2dim  32551  ps-1  32558  paddclN  32923  ltrnnid  33217  cdleme22b  33422  dihmeetlem13N  34401  dih1dimatlem  34411  dihlspsnat  34415
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 179
  Copyright terms: Public domain W3C validator