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

Theorem syl5ib 234
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 219 . 2 (𝜒 → (𝜓𝜃))
41, 3syl5 34 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  syl5ibcom  235  syl5ibr  236  dvelimdf  2475  sb4  2493  sbft  2516  gencl  3375  vtoclgft  3394  spsbc  3589  eqsbc3rOLD  3634  ssnelpss  3860  dfnfc2  4606  uniintsn  4666  prex  5058  copsexg  5104  posn  5344  optocl  5352  ordtri3OLD  5921  funimass1  6132  f1ocnvb  6312  eqfnfv2  6476  elpreima  6501  fconst5  6636  dff13  6676  f1ocnvfv  6698  f1ocnvfvb  6699  fliftfun  6726  eusvobj2  6807  sorpsscmpl  7114  ssonprc  7158  xpexr  7272  xpexcnv  7274  relcnvexb  7280  dmfex  7290  frxp  7456  mpt2xopn0yelv  7509  rntpos  7535  oawordeulem  7805  oalimcl  7811  odi  7830  omeulem2  7834  oeeulem  7852  erexb  7938  unxpdomlem2  8332  dif1en  8360  enp1ilem  8361  findcard2  8367  isfinite2  8385  unfi  8394  fodomfib  8407  inf0  8693  rankxplim2  8918  scott0  8924  ficardom  8997  cardaleph  9122  dfac5  9161  cflim2  9297  fin23lem23  9360  fin23lem28  9374  isf32lem5  9391  domtriomlem  9476  ac6num  9513  zorn2lem5  9534  zorn2lem6  9535  iunfo  9573  axrepndlem2  9627  axregnd  9638  hargch  9707  addcanpi  9933  mulcanpi  9934  indpi  9941  ltaddnq  10008  ltexnq  10009  prlem934  10067  ltaddpr2  10069  ltaprlem  10078  supsrlem  10144  ssxr  10319  ltxrlt  10320  addcan  10432  addcan2  10433  neg11  10544  negreb  10558  mulcand  10872  receu  10884  lemul1a  11089  cju  11228  nn1suc  11253  nnaddcl  11254  nndivtr  11274  znegclb  11626  zmulcl  11638  zeo  11675  uz11  11922  uzp1  11934  eqreznegel  11987  rpnnen1lem6  12032  rpnnen1OLD  12038  xrltne  12207  xneg11  12259  xnegdi  12291  xrsupss  12352  xrinfmss  12353  elfznelfzob  12788  modadd1  12921  modmul1  12937  om2uzlti  12963  bccmpl  13310  hashen  13349  fz1eqb  13357  hashfn  13376  hashnn0n0nn  13392  hashtpg  13479  eqwrd  13553  ccatopth  13690  ccatopth2  13691  swrdccatin2  13707  swrdccat3a  13714  cj11  14121  rennim  14198  cnpart  14199  sqrmo  14211  sqrtgt0  14218  sqreulem  14318  sqreu  14319  lo1o1  14482  lo1eq  14518  rlimeq  14519  sumss  14674  cvgcmp  14767  fprodser  14898  efne0  15046  dvdsabseq  15257  divalglem8  15345  bitsinv1lem  15385  pcfac  15825  prmreclem3  15844  sectmon  16663  yoniso  17146  lublecllem  17209  oduposb  17357  mgmb1mgm1  17475  sgrp2rid2  17634  grpinveu  17677  mulgass  17800  galcan  17957  symg1bas  18036  cayleylem2  18053  odbezout  18195  odeq1  18197  dprddomcld  18620  dvreq1  18913  unitrrg  19515  coe1tm  19865  frgpcyg  20144  obslbs  20296  tgss3  21012  uptx  21650  txindislem  21658  qtopeu  21741  hmeocnvb  21799  qtophmeo  21842  trufil  21935  ufinffr  21954  ghmcnp  22139  tgioo  22820  lmmcvg  23279  bcth3  23348  ovolunlem1a  23484  vitali  23601  ismbf  23616  ismbfcn  23617  rolle  23972  itgsubstlem  24030  vieta1lem2  24285  elqaalem3  24295  aacjcl  24301  efif1olem4  24511  lognegb  24556  logcj  24572  argimgt0  24578  logdmnrp  24607  logcnlem3  24610  logrec  24721  dcubic  24793  isppw  25060  rplogsumlem2  25394  pntpbnd1  25495  axlowdimlem16  26057  usgr0vb  26349  nbgrssvwo2  26478  nbgrssvwo2OLD  26481  redwlk  26800  usgr2pthspth  26889  usgr2pth  26891  wlkpwwlkf1ouspgr  27009  wlklnwwlkln2lem  27012  wpthswwlks2on  27103  clwlkclwwlkf  27152  wwlksubclwwlk  27210  frgr0v  27436  grpoinveu  27703  grpoinvf  27716  diporthcom  27901  norm1exi  28437  shmodsi  28578  shmodi  28579  dfch2  28596  orthin  28635  chssoc  28685  spansncvi  28841  kbpj  29145  lnopunilem1  29199  cnlnssadj  29269  bra11  29297  strlem4  29443  strlem5  29444  hstrlem4  29451  hstrlem5  29452  dmdmd  29489  mdslle1i  29506  mdslle2i  29507  mdslmd1lem1  29514  atcvatlem  29574  atcvat4i  29586  mdsymlem3  29594  bcm1n  29884  xmulcand  29959  xreceu  29960  tpr2rico  30288  bnj1125  31388  mrsubff1  31739  mvhf1  31784  funpsstri  31991  sltres  32142  nosupno  32176  nosupres  32180  btwnintr  32453  idinside  32518  btwnconn1lem13  32533  fneval  32674  bj-sbftv  33091  bj-equsal1t  33137  bj-ldiv  33484  bj-bary1lem1  33490  bj-bary1  33491  wl-equsal1i  33660  uncf  33719  matunitlindflem2  33737  poimirlem4  33744  poimirlem9  33749  ismtybndlem  33936  grpoeqdivid  34011  0rngo  34157  ax12indalem  34752  ax12inda2ALT  34753  lcvexchlem4  34845  lcvexchlem5  34846  opcon3b  35004  2dim  35277  ps-1  35284  paddclN  35649  ltrnnid  35943  cdleme22b  36149  dihmeetlem13N  37128  dih1dimatlem  37138  dihlspsnat  37142  frege58c  38735  sscon34b  38837  gneispa  38948  nzss  39036  expgrowth  39054  sbiota1  39155  sbgoldbwt  42193  dignn0flhalflem1  42937  aacllem  43078
  Copyright terms: Public domain W3C validator