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

Theorem syl5ib 235
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 220 . 2 (𝜒 → (𝜓𝜃))
41, 3syl5 34 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  syl5ibcom  236  syl5ibr  237  dvelimdf  2499  sb4  2517  sbft  2540  gencl  3440  vtoclgft  3459  spsbc  3657  ssnelpss  3927  dfnfc2  4661  uniintsn  4717  prex  5110  copsexg  5156  posn  5400  optocl  5408  funimass1  6189  f1ocnvb  6373  eqfnfv2  6541  elpreima  6566  fconst5  6703  dff13  6743  f1ocnvfv  6765  f1ocnvfvb  6766  fliftfun  6793  eusvobj2  6874  sorpsscmpl  7185  ssonprc  7229  xpexr  7343  xpexcnv  7345  relcnvexb  7351  dmfex  7361  frxp  7528  mpt2xopn0yelv  7581  rntpos  7607  oawordeulem  7878  oalimcl  7884  odi  7903  omeulem2  7907  oeeulem  7925  erexb  8011  unxpdomlem2  8411  dif1en  8439  enp1ilem  8440  findcard2  8446  isfinite2  8464  unfi  8473  fodomfib  8486  inf0  8772  rankxplim2  8997  scott0  9003  ficardom  9077  cardaleph  9202  dfac5  9241  cflim2  9377  fin23lem23  9440  fin23lem28  9454  isf32lem5  9471  domtriomlem  9556  ac6num  9593  zorn2lem5  9614  zorn2lem6  9615  iunfo  9653  axrepndlem2  9707  axregnd  9718  hargch  9787  addcanpi  10013  mulcanpi  10014  indpi  10021  ltaddnq  10088  ltexnq  10089  prlem934  10147  ltaddpr2  10149  ltaprlem  10158  supsrlem  10224  ssxr  10399  ltxrlt  10400  addcan  10512  addcan2  10513  neg11  10624  negreb  10638  mulcand  10952  receu  10964  lemul1a  11169  cju  11308  nn1suc  11333  nnaddcl  11334  nndivtr  11355  znegclb  11687  zmulcl  11699  zeo  11736  uz11  11934  uzp1  11946  eqreznegel  12000  rpnnen1lem6  12045  xrltne  12219  xneg11  12271  xnegdi  12303  xrsupss  12364  xrinfmss  12365  elfznelfzob  12805  modadd1  12938  modmul1  12954  om2uzlti  12980  bccmpl  13323  hashen  13362  fz1eqb  13370  hashfn  13389  hashnn0n0nn  13405  hashtpg  13491  eqwrd  13565  ccatopth  13701  ccatopth2  13702  swrdccatin2  13718  swrdccat3a  13725  cj11  14132  rennim  14209  cnpart  14210  sqrmo  14222  sqrtgt0  14229  sqreulem  14329  sqreu  14330  lo1o1  14493  lo1eq  14529  rlimeq  14530  sumss  14685  cvgcmp  14777  fprodser  14907  efne0  15054  dvdsabseq  15265  divalglem8  15350  bitsinv1lem  15389  pcfac  15827  prmreclem3  15846  sectmon  16653  yoniso  17137  lublecllem  17200  oduposb  17348  mgmb1mgm1  17466  sgrp2rid2  17625  grpinveu  17668  mulgass  17788  galcan  17945  symg1bas  18024  cayleylem2  18041  odbezout  18183  odeq1  18185  dprddomcld  18609  dvreq1  18902  unitrrg  19509  coe1tm  19858  frgpcyg  20136  obslbs  20292  tgss3  21012  uptx  21650  txindislem  21658  qtopeu  21741  hmeocnvb  21799  qtophmeo  21842  trufil  21935  ufinffr  21954  ghmcnp  22139  tgioo  22820  lmmcvg  23280  bcth3  23349  ovolunlem1a  23487  vitali  23604  ismbf  23619  ismbfcn  23620  rolle  23977  itgsubstlem  24035  vieta1lem2  24290  elqaalem3  24300  aacjcl  24306  efif1olem4  24516  lognegb  24560  logcj  24576  argimgt0  24582  logdmnrp  24611  logcnlem3  24614  logrec  24725  dcubic  24797  isppw  25064  rplogsumlem2  25398  pntpbnd1  25499  axlowdimlem16  26061  usgr0vb  26355  nbgrssvwo2  26484  nbgrssvwo2OLD  26487  redwlk  26807  usgr2pthspth  26896  usgr2pth  26898  wlkswwlksf1o  27016  wlklnwwlkln2lem  27019  wpthswwlks2on  27112  clwlkclwwlkf  27161  wwlksubclwwlk  27219  frgr0v  27446  grpoinveu  27712  grpoinvf  27725  diporthcom  27909  norm1exi  28445  shmodsi  28586  shmodi  28587  dfch2  28604  orthin  28643  chssoc  28693  spansncvi  28849  kbpj  29153  lnopunilem1  29207  cnlnssadj  29277  bra11  29305  strlem4  29451  strlem5  29452  hstrlem4  29459  hstrlem5  29460  dmdmd  29497  mdslle1i  29514  mdslle2i  29515  mdslmd1lem1  29522  atcvatlem  29582  atcvat4i  29594  mdsymlem3  29602  bcm1n  29891  xmulcand  29964  xreceu  29965  tpr2rico  30293  bnj1125  31392  mrsubff1  31743  mvhf1  31788  funpsstri  31994  sltres  32145  nosupno  32179  nosupres  32183  btwnintr  32456  idinside  32521  btwnconn1lem13  32536  fneval  32677  bj-sbftv  33085  bj-equsal1t  33128  bj-ldiv  33478  bj-bary1lem1  33484  bj-bary1  33485  wl-equsal1i  33649  uncf  33707  matunitlindflem2  33725  poimirlem4  33732  poimirlem9  33737  ismtybndlem  33922  grpoeqdivid  33997  0rngo  34143  ax12indalem  34730  ax12inda2ALT  34731  lcvexchlem4  34823  lcvexchlem5  34824  opcon3b  34982  2dim  35256  ps-1  35263  paddclN  35628  ltrnnid  35922  cdleme22b  36127  dihmeetlem13N  37105  dih1dimatlem  37115  dihlspsnat  37119  frege58c  38720  sscon34b  38822  gneispa  38933  nzss  39021  expgrowth  39039  sbiota1  39139  fafv2elrnb  41829  sbgoldbwt  42245  dignn0flhalflem1  42982  aacllem  43123
  Copyright terms: Public domain W3C validator