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  2334  sb4  2355  sbft  2378  gencl  3225  vtoclgft  3244  spsbc  3435  eqsbc3rOLD  3480  ssnelpss  3702  dfnfc2  4427  uniintsn  4486  prex  4880  copsexg  4926  posn  5158  optocl  5166  ordtri3OLD  5729  funimass1  5939  f1ocnvb  6117  eqfnfv2  6278  elpreima  6303  fconst5  6436  dff13  6477  f1ocnvfv  6499  f1ocnvfvb  6500  fliftfun  6527  eusvobj2  6608  sorpsscmpl  6913  ssonprc  6954  xpexr  7068  xpexcnv  7070  relcnvexb  7076  dmfex  7086  frxp  7247  mpt2xopn0yelv  7299  rntpos  7325  oawordeulem  7594  oalimcl  7600  odi  7619  omeulem2  7623  oeeulem  7641  erexb  7727  unxpdomlem2  8125  dif1en  8153  enp1ilem  8154  findcard2  8160  isfinite2  8178  unfi  8187  fodomfib  8200  inf0  8478  rankxplim2  8703  scott0  8709  ficardom  8747  cardaleph  8872  dfac5  8911  cflim2  9045  fin23lem23  9108  fin23lem28  9122  isf32lem5  9139  domtriomlem  9224  ac6num  9261  zorn2lem5  9282  zorn2lem6  9283  iunfo  9321  axrepndlem2  9375  axregnd  9386  hargch  9455  addcanpi  9681  mulcanpi  9682  indpi  9689  ltaddnq  9756  ltexnq  9757  prlem934  9815  ltaddpr2  9817  ltaprlem  9826  supsrlem  9892  ssxr  10067  ltxrlt  10068  addcan  10180  addcan2  10181  neg11  10292  negreb  10306  mulcand  10620  receu  10632  lemul1a  10837  cju  10976  nn1suc  11001  nnaddcl  11002  nndivtr  11022  znegclb  11374  zmulcl  11386  zeo  11423  uz11  11670  uzp1  11681  eqreznegel  11734  rpnnen1lem6  11779  rpnnen1OLD  11785  xrltne  11954  xneg11  12005  xnegdi  12037  xrsupss  12098  xrinfmss  12099  elfznelfzob  12531  modadd1  12663  modmul1  12679  om2uzlti  12705  bccmpl  13052  hashen  13091  fz1eqb  13101  hashfn  13120  hashnn0n0nn  13136  hashtpg  13221  eqwrd  13301  ccatopth  13424  ccatopth2  13425  swrdccatin2  13440  swrdccat3a  13447  cj11  13852  rennim  13929  cnpart  13930  sqrmo  13942  sqrtgt0  13949  sqreulem  14049  sqreu  14050  lo1o1  14213  lo1eq  14249  rlimeq  14250  sumss  14404  cvgcmp  14494  fprodser  14623  efne0  14771  dvdsabseq  14978  divalglem8  15066  bitsinv1lem  15106  pcfac  15546  prmreclem3  15565  sectmon  16382  yoniso  16865  lublecllem  16928  oduposb  17076  mgmb1mgm1  17194  sgrp2rid2  17353  grpinveu  17396  mulgass  17519  galcan  17677  symg1bas  17756  cayleylem2  17773  odbezout  17915  odeq1  17917  dprddomcld  18340  dvreq1  18633  unitrrg  19233  coe1tm  19583  frgpcyg  19862  obslbs  20014  tgss3  20730  uptx  21368  txindislem  21376  qtopeu  21459  hmeocnvb  21517  qtophmeo  21560  trufil  21654  ufinffr  21673  ghmcnp  21858  tgioo  22539  lmmcvg  22999  bcth3  23068  ovolunlem1a  23204  vitali  23322  ismbf  23337  ismbfcn  23338  rolle  23691  itgsubstlem  23749  vieta1lem2  24004  elqaalem3  24014  aacjcl  24020  efif1olem4  24229  lognegb  24274  logcj  24290  argimgt0  24296  logdmnrp  24321  logcnlem3  24324  logrec  24435  dcubic  24507  isppw  24774  rplogsumlem2  25108  pntpbnd1  25209  axlowdimlem16  25771  usgr0vb  26056  nbgrssvwo2  26182  redwlk  26472  usgr2pthspth  26561  usgr2pth  26563  wlkpwwlkf1ouspgr  26668  wlklnwwlkln2lem  26671  wwlksubclwwlks  26825  frgr0v  27025  frgr2wwlk1  27086  grpoinveu  27261  grpoinvf  27274  diporthcom  27459  norm1exi  27995  shmodsi  28136  shmodi  28137  dfch2  28154  orthin  28193  chssoc  28243  spansncvi  28399  kbpj  28703  lnopunilem1  28757  cnlnssadj  28827  bra11  28855  strlem4  29001  strlem5  29002  hstrlem4  29009  hstrlem5  29010  dmdmd  29047  mdslle1i  29064  mdslle2i  29065  mdslmd1lem1  29072  atcvatlem  29132  atcvat4i  29144  mdsymlem3  29152  bcm1n  29437  xmulcand  29456  xreceu  29457  tpr2rico  29782  bnj1125  30821  mrsubff1  31172  mvhf1  31217  funpsstri  31420  sltres  31571  noreslege  31624  nosino  31628  nosires  31630  btwnintr  31821  idinside  31886  btwnconn1lem13  31901  fneval  32042  bj-sbftv  32459  bj-equsal1t  32505  bj-ldiv  32827  bj-bary1lem1  32833  bj-bary1  32834  wl-equsal1i  33000  uncf  33059  matunitlindflem2  33077  poimirlem4  33084  poimirlem9  33089  ismtybndlem  33276  grpoeqdivid  33351  0rngo  33497  ax12indalem  33749  ax12inda2ALT  33750  lcvexchlem4  33843  lcvexchlem5  33844  opcon3b  34002  2dim  34275  ps-1  34282  paddclN  34647  ltrnnid  34941  cdleme22b  35148  dihmeetlem13N  36127  dih1dimatlem  36137  dihlspsnat  36141  frege58c  37736  sscon34b  37838  gneispa  37949  nzss  38037  expgrowth  38055  sbiota1  38156  bgoldbwt  40990  dignn0flhalflem1  41731  aacllem  41880
  Copyright terms: Public domain W3C validator