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

Theorem syl5ib 245
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 230 . 2 (𝜒 → (𝜓𝜃))
41, 3syl5 34 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  syl5ibcom  246  syl5ibr  247  sbft  2261  dvelimdf  2466  sb4ALT  2584  sbftALT  2589  gencl  3535  vtoclgft  3554  vtoclgftOLD  3555  spsbc  3784  ssnelpss  4087  dfnfc2  4850  uniintsn  4906  prex  5324  copsexgw  5373  copsexg  5374  posn  5631  optocl  5639  funimass1  6430  f1ocnvb  6622  eqfnfv2  6796  elpreima  6821  fconst5  6961  dff13  7004  f1ocnvfv  7026  f1ocnvfvb  7027  fliftfun  7054  eusvobj2  7138  sorpsscmpl  7449  ssonprc  7495  xpexr  7611  xpexcnv  7613  relcnvexb  7619  dmfex  7629  frxp  7811  mpoxopn0yelv  7870  rntpos  7896  oawordeulem  8170  oalimcl  8176  odi  8195  omeulem2  8199  oeeulem  8217  erexb  8304  unxpdomlem2  8712  dif1en  8740  enp1ilem  8741  findcard2  8747  isfinite2  8765  unfi  8774  fodomfib  8787  inf0  9073  rankxplim2  9298  scott0  9304  djuexb  9327  ficardom  9379  cardaleph  9504  dfac5  9543  cflim2  9674  fin23lem23  9737  fin23lem28  9751  isf32lem5  9768  domtriomlem  9853  ac6num  9890  zorn2lem5  9911  zorn2lem6  9912  iunfo  9950  axrepndlem2  10004  axregnd  10015  hargch  10084  addcanpi  10310  mulcanpi  10311  indpi  10318  ltaddnq  10385  ltexnq  10386  prlem934  10444  ltaddpr2  10446  ltaprlem  10455  supsrlem  10522  ssxr  10699  ltxrlt  10700  addcan  10813  addcan2  10814  neg11  10926  negreb  10940  mulcand  11262  receu  11274  ldiv  11463  lemul1a  11483  cju  11623  nn1suc  11648  nnaddcl  11649  nndivtr  11673  znegclb  12008  zmulcl  12020  zeo  12057  uz11  12256  uzp1  12268  eqreznegel  12323  rpnnen1lem6  12371  xrltne  12546  xneg11  12598  xnegdi  12631  xrsupss  12692  xrinfmss  12693  elfznelfzob  13133  modadd1  13266  modmul1  13282  om2uzlti  13308  bccmpl  13659  hashen  13697  fz1eqb  13705  hashfn  13726  hashnn0n0nn  13742  hashtpg  13833  eqwrd  13899  ccatopth  14068  ccatopth2  14069  swrdccatin2  14081  cj11  14511  rennim  14588  cnpart  14589  sqrmo  14601  sqrtgt0  14608  sqreulem  14709  sqreu  14710  cnsqrt00  14742  lo1o1  14879  lo1eq  14915  rlimeq  14916  sumss  15071  cvgcmp  15161  fprodser  15293  efne0  15440  dvdsabseq  15653  divalglem8  15741  bitsinv1lem  15780  pcfac  16225  prmreclem3  16244  sectmon  17042  yoniso  17525  lublecllem  17588  oduposb  17736  mgmb1mgm1  17855  sgrp2rid2  18031  grpinveu  18078  mulgass  18204  galcan  18374  symg1bas  18455  cayleylem2  18472  odbezout  18616  odeq1  18618  dprddomcld  19054  dvreq1  19374  unitrrg  19996  coe1tm  20371  frgpcyg  20650  obslbs  20804  tgss3  21524  uptx  22163  txindislem  22171  qtopeu  22254  hmeocnvb  22312  qtophmeo  22355  trufil  22448  ufinffr  22467  ghmcnp  22652  tgioo  23333  lmmcvg  23793  bcth3  23863  ovolunlem1a  24026  vitali  24143  ismbf  24158  ismbfcn  24159  rolle  24516  itgsubstlem  24574  vieta1lem2  24829  elqaalem3  24839  aacjcl  24845  efif1olem4  25056  lognegb  25100  logcj  25116  argimgt0  25122  logdmnrp  25151  logcnlem3  25154  logrec  25268  dcubic  25351  isppw  25619  rplogsumlem2  25989  pntpbnd1  26090  axlowdimlem16  26671  usgr0vb  26947  nbgrssvwo2  27072  redwlk  27382  usgr2pthspth  27471  usgr2pth  27473  wlkswwlksf1o  27585  wlklnwwlkln2lem  27588  wpthswwlks2on  27668  clwlkclwwlkf  27714  wwlksubclwwlk  27765  frgr0v  27969  grpoinveu  28224  grpoinvf  28237  diporthcom  28421  norm1exi  28955  shmodsi  29094  shmodi  29095  dfch2  29112  orthin  29151  chssoc  29201  spansncvi  29357  kbpj  29661  lnopunilem1  29715  cnlnssadj  29785  bra11  29813  strlem4  29959  strlem5  29960  hstrlem4  29967  hstrlem5  29968  dmdmd  30005  mdslle1i  30022  mdslle2i  30023  mdslmd1lem1  30030  atcvatlem  30090  atcvat4i  30102  mdsymlem3  30110  bcm1n  30445  xmulcand  30525  xreceu  30526  tpr2rico  31055  bnj1125  32162  revwlkb  32270  umgr2cycllem  32285  mrsubff1  32659  mvhf1  32704  funpsstri  32906  sltres  33067  nosupno  33101  nosupres  33105  btwnintr  33378  idinside  33443  btwnconn1lem13  33458  fneval  33598  bj-equsal1t  34043  bj-brrelex12ALT  34254  bj-elid6  34355  bj-isrvec2  34470  bj-bary1lem1  34481  bj-bary1  34482  fvineqsnf1  34574  wl-equsal1i  34665  uncf  34753  matunitlindflem2  34771  poimirlem4  34778  poimirlem9  34783  ismtybndlem  34967  grpoeqdivid  35042  0rngo  35188  imaexALTV  35470  dmqseqim  35772  ax12indalem  35963  ax12inda2ALT  35964  lcvexchlem4  36055  lcvexchlem5  36056  opcon3b  36214  2dim  36488  ps-1  36495  paddclN  36860  ltrnnid  37154  cdleme22b  37359  dihmeetlem13N  38337  dih1dimatlem  38347  dihlspsnat  38351  remulcan2d  39036  nnaddcom  39041  frege58c  40147  sscon34b  40249  gneispa  40360  nzss  40529  expgrowth  40547  sbiota1  40646  fafv2elrnb  43315  sbgoldbwt  43789  dignn0flhalflem1  44573  rrxlinesc  44620  aacllem  44800
  Copyright terms: Public domain W3C validator