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

Theorem syl5ib 246
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 231 . 2 (𝜒 → (𝜓𝜃))
41, 3syl5 34 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208
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 209
This theorem is referenced by:  syl5ibcom  247  syl5ibr  248  sbft  2266  dvelimdf  2467  sb4ALT  2584  sbftALT  2589  gencl  3534  vtoclgft  3553  vtoclgftOLD  3554  spsbc  3784  ssnelpss  4087  dfnfc2  4859  uniintsn  4912  prex  5332  copsexgw  5380  copsexg  5381  posn  5636  optocl  5644  funimass1  6435  f1ocnvb  6627  eqfnfv2  6802  elpreima  6827  fconst5  6967  dff13  7012  f1ocnvfv  7034  f1ocnvfvb  7035  fliftfun  7064  eusvobj2  7148  sorpsscmpl  7459  ssonprc  7506  xpexr  7622  xpexcnv  7624  relcnvexb  7630  dmfex  7640  frxp  7819  mpoxopn0yelv  7878  rntpos  7904  oawordeulem  8179  oalimcl  8185  odi  8204  omeulem2  8208  oeeulem  8226  erexb  8313  unxpdomlem2  8722  dif1en  8750  enp1ilem  8751  findcard2  8757  isfinite2  8775  unfi  8784  fodomfib  8797  inf0  9083  rankxplim2  9308  scott0  9314  djuexb  9337  ficardom  9389  cardaleph  9514  dfac5  9553  cflim2  9684  fin23lem23  9747  fin23lem28  9761  isf32lem5  9778  domtriomlem  9863  ac6num  9900  zorn2lem5  9921  zorn2lem6  9922  iunfo  9960  axrepndlem2  10014  axregnd  10025  hargch  10094  addcanpi  10320  mulcanpi  10321  indpi  10328  ltaddnq  10395  ltexnq  10396  prlem934  10454  ltaddpr2  10456  ltaprlem  10465  supsrlem  10532  ssxr  10709  ltxrlt  10710  addcan  10823  addcan2  10824  neg11  10936  negreb  10950  mulcand  11272  receu  11284  ldiv  11473  lemul1a  11493  cju  11633  nn1suc  11658  nnaddcl  11659  nndivtr  11683  znegclb  12018  zmulcl  12030  zeo  12067  uz11  12266  uzp1  12278  eqreznegel  12333  rpnnen1lem6  12380  xrltne  12555  xneg11  12607  xnegdi  12640  xrsupss  12701  xrinfmss  12702  elfznelfzob  13142  modadd1  13275  modmul1  13291  om2uzlti  13317  bccmpl  13668  hashen  13706  fz1eqb  13714  hashfn  13735  hashnn0n0nn  13751  hashtpg  13842  eqwrd  13908  ccatopth  14077  ccatopth2  14078  swrdccatin2  14090  cj11  14520  rennim  14597  cnpart  14598  sqrmo  14610  sqrtgt0  14617  sqreulem  14718  sqreu  14719  cnsqrt00  14751  lo1o1  14888  lo1eq  14924  rlimeq  14925  sumss  15080  cvgcmp  15170  fprodser  15302  efne0  15449  dvdsabseq  15662  divalglem8  15750  bitsinv1lem  15789  pcfac  16234  prmreclem3  16253  sectmon  17051  yoniso  17534  lublecllem  17597  oduposb  17745  mgmb1mgm1  17864  sgrp2rid2  18090  grpinveu  18137  mulgass  18263  galcan  18433  symg1bas  18518  cayleylem2  18540  odbezout  18684  odeq1  18686  dprddomcld  19122  dvreq1  19442  unitrrg  20065  coe1tm  20440  frgpcyg  20719  obslbs  20873  tgss3  21593  uptx  22232  txindislem  22240  qtopeu  22323  hmeocnvb  22381  qtophmeo  22424  trufil  22517  ufinffr  22536  ghmcnp  22722  tgioo  23403  lmmcvg  23863  bcth3  23933  ovolunlem1a  24096  vitali  24213  ismbf  24228  ismbfcn  24229  rolle  24586  itgsubstlem  24644  vieta1lem2  24899  elqaalem3  24909  aacjcl  24915  efif1olem4  25128  lognegb  25172  logcj  25188  argimgt0  25194  logdmnrp  25223  logcnlem3  25226  logrec  25340  dcubic  25423  isppw  25690  rplogsumlem2  26060  pntpbnd1  26161  axlowdimlem16  26742  usgr0vb  27018  nbgrssvwo2  27143  redwlk  27453  usgr2pthspth  27542  usgr2pth  27544  wlkswwlksf1o  27656  wlklnwwlkln2lem  27659  wpthswwlks2on  27739  clwlkclwwlkf  27785  wwlksubclwwlk  27836  frgr0v  28040  grpoinveu  28295  grpoinvf  28308  diporthcom  28492  norm1exi  29026  shmodsi  29165  shmodi  29166  dfch2  29183  orthin  29222  chssoc  29272  spansncvi  29428  kbpj  29732  lnopunilem1  29786  cnlnssadj  29856  bra11  29884  strlem4  30030  strlem5  30031  hstrlem4  30038  hstrlem5  30039  dmdmd  30076  mdslle1i  30093  mdslle2i  30094  mdslmd1lem1  30101  atcvatlem  30161  atcvat4i  30173  mdsymlem3  30181  bcm1n  30517  xmulcand  30597  xreceu  30598  tpr2rico  31155  bnj1125  32264  revwlkb  32372  umgr2cycllem  32387  mrsubff1  32761  mvhf1  32806  funpsstri  33008  sltres  33169  nosupno  33203  nosupres  33207  btwnintr  33480  idinside  33545  btwnconn1lem13  33560  fneval  33700  bj-equsal1t  34145  bj-brrelex12ALT  34358  bj-elid6  34461  bj-isrvec2  34580  bj-bary1lem1  34591  bj-bary1  34592  fvineqsnf1  34690  wl-equsal1i  34782  uncf  34870  matunitlindflem2  34888  poimirlem4  34895  poimirlem9  34900  ismtybndlem  35083  grpoeqdivid  35158  0rngo  35304  imaexALTV  35586  dmqseqim  35889  ax12indalem  36080  ax12inda2ALT  36081  lcvexchlem4  36172  lcvexchlem5  36173  opcon3b  36331  2dim  36605  ps-1  36612  paddclN  36977  ltrnnid  37271  cdleme22b  37476  dihmeetlem13N  38454  dih1dimatlem  38464  dihlspsnat  38468  remulcan2d  39156  nnaddcom  39161  frege58c  40267  sscon34b  40369  gneispa  40480  nzss  40649  expgrowth  40667  sbiota1  40766  fafv2elrnb  43435  sbgoldbwt  43943  dignn0flhalflem1  44676  rrxlinesc  44723  aacllem  44903
  Copyright terms: Public domain W3C validator