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  2333  sb4  2354  sbft  2377  gencl  3230  vtoclgft  3249  spsbc  3442  eqsbc3rOLD  3487  ssnelpss  3710  dfnfc2  4445  uniintsn  4505  prex  4900  copsexg  4946  posn  5177  optocl  5185  ordtri3OLD  5748  funimass1  5959  f1ocnvb  6137  eqfnfv2  6298  elpreima  6323  fconst5  6456  dff13  6497  f1ocnvfv  6519  f1ocnvfvb  6520  fliftfun  6547  eusvobj2  6628  sorpsscmpl  6933  ssonprc  6977  xpexr  7091  xpexcnv  7093  relcnvexb  7099  dmfex  7109  frxp  7272  mpt2xopn0yelv  7324  rntpos  7350  oawordeulem  7619  oalimcl  7625  odi  7644  omeulem2  7648  oeeulem  7666  erexb  7752  unxpdomlem2  8150  dif1en  8178  enp1ilem  8179  findcard2  8185  isfinite2  8203  unfi  8212  fodomfib  8225  inf0  8503  rankxplim2  8728  scott0  8734  ficardom  8772  cardaleph  8897  dfac5  8936  cflim2  9070  fin23lem23  9133  fin23lem28  9147  isf32lem5  9164  domtriomlem  9249  ac6num  9286  zorn2lem5  9307  zorn2lem6  9308  iunfo  9346  axrepndlem2  9400  axregnd  9411  hargch  9480  addcanpi  9706  mulcanpi  9707  indpi  9714  ltaddnq  9781  ltexnq  9782  prlem934  9840  ltaddpr2  9842  ltaprlem  9851  supsrlem  9917  ssxr  10092  ltxrlt  10093  addcan  10205  addcan2  10206  neg11  10317  negreb  10331  mulcand  10645  receu  10657  lemul1a  10862  cju  11001  nn1suc  11026  nnaddcl  11027  nndivtr  11047  znegclb  11399  zmulcl  11411  zeo  11448  uz11  11695  uzp1  11706  eqreznegel  11759  rpnnen1lem6  11804  rpnnen1OLD  11810  xrltne  11979  xneg11  12031  xnegdi  12063  xrsupss  12124  xrinfmss  12125  elfznelfzob  12558  modadd1  12690  modmul1  12706  om2uzlti  12732  bccmpl  13079  hashen  13118  fz1eqb  13128  hashfn  13147  hashnn0n0nn  13163  hashtpg  13250  eqwrd  13329  ccatopth  13452  ccatopth2  13453  swrdccatin2  13468  swrdccat3a  13475  cj11  13883  rennim  13960  cnpart  13961  sqrmo  13973  sqrtgt0  13980  sqreulem  14080  sqreu  14081  lo1o1  14244  lo1eq  14280  rlimeq  14281  sumss  14436  cvgcmp  14529  fprodser  14660  efne0  14808  dvdsabseq  15016  divalglem8  15104  bitsinv1lem  15144  pcfac  15584  prmreclem3  15603  sectmon  16423  yoniso  16906  lublecllem  16969  oduposb  17117  mgmb1mgm1  17235  sgrp2rid2  17394  grpinveu  17437  mulgass  17560  galcan  17718  symg1bas  17797  cayleylem2  17814  odbezout  17956  odeq1  17958  dprddomcld  18381  dvreq1  18674  unitrrg  19274  coe1tm  19624  frgpcyg  19903  obslbs  20055  tgss3  20771  uptx  21409  txindislem  21417  qtopeu  21500  hmeocnvb  21558  qtophmeo  21601  trufil  21695  ufinffr  21714  ghmcnp  21899  tgioo  22580  lmmcvg  23040  bcth3  23109  ovolunlem1a  23245  vitali  23363  ismbf  23378  ismbfcn  23379  rolle  23734  itgsubstlem  23792  vieta1lem2  24047  elqaalem3  24057  aacjcl  24063  efif1olem4  24272  lognegb  24317  logcj  24333  argimgt0  24339  logdmnrp  24368  logcnlem3  24371  logrec  24482  dcubic  24554  isppw  24821  rplogsumlem2  25155  pntpbnd1  25256  axlowdimlem16  25818  usgr0vb  26110  nbgrssvwo2  26242  redwlk  26550  usgr2pthspth  26639  usgr2pth  26641  wlkpwwlkf1ouspgr  26746  wlklnwwlkln2lem  26749  wwlksubclwwlks  26905  frgr0v  27105  grpoinveu  27343  grpoinvf  27356  diporthcom  27541  norm1exi  28077  shmodsi  28218  shmodi  28219  dfch2  28236  orthin  28275  chssoc  28325  spansncvi  28481  kbpj  28785  lnopunilem1  28839  cnlnssadj  28909  bra11  28937  strlem4  29083  strlem5  29084  hstrlem4  29091  hstrlem5  29092  dmdmd  29129  mdslle1i  29146  mdslle2i  29147  mdslmd1lem1  29154  atcvatlem  29214  atcvat4i  29226  mdsymlem3  29234  bcm1n  29528  xmulcand  29603  xreceu  29604  tpr2rico  29932  bnj1125  31034  mrsubff1  31385  mvhf1  31430  funpsstri  31639  sltres  31789  nosupno  31823  nosupres  31827  btwnintr  32101  idinside  32166  btwnconn1lem13  32181  fneval  32322  bj-sbftv  32738  bj-equsal1t  32784  bj-ldiv  33126  bj-bary1lem1  33132  bj-bary1  33133  wl-equsal1i  33300  uncf  33359  matunitlindflem2  33377  poimirlem4  33384  poimirlem9  33389  ismtybndlem  33576  grpoeqdivid  33651  0rngo  33797  ax12indalem  34049  ax12inda2ALT  34050  lcvexchlem4  34143  lcvexchlem5  34144  opcon3b  34302  2dim  34575  ps-1  34582  paddclN  34947  ltrnnid  35241  cdleme22b  35448  dihmeetlem13N  36427  dih1dimatlem  36437  dihlspsnat  36441  frege58c  38035  sscon34b  38137  gneispa  38248  nzss  38336  expgrowth  38354  sbiota1  38455  sbgoldbwt  41430  dignn0flhalflem1  42174  aacllem  42312
  Copyright terms: Public domain W3C validator