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

Theorem syl5ib 232
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 217 . 2 (𝜒 → (𝜓𝜃))
41, 3syl5 33 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  syl5ibcom  233  syl5ibr  234  dvelimdf  2319  sb4  2340  sbft  2363  gencl  3204  vtoclgft  3223  spsbc  3411  eqsbc3rOLD  3456  ssnelpss  3676  dfnfc2  4381  uniintsn  4440  prex  4828  copsexg  4873  posn  5097  optocl  5105  ordtri3OLD  5660  funimass1  5868  f1ocnvb  6045  eqfnfv2  6202  elpreima  6227  fconst5  6351  dff13  6391  f1ocnvfv  6409  f1ocnvfvb  6410  fliftfun  6437  eusvobj2  6517  sorpsscmpl  6820  ssonprc  6858  xpexr  6973  xpexcnv  6975  relcnvexb  6981  dmfex  6991  frxp  7148  mpt2xopn0yelv  7200  rntpos  7226  oawordeulem  7495  oalimcl  7501  odi  7520  omeulem2  7524  oeeulem  7542  erexb  7628  unxpdomlem2  8024  dif1en  8052  enp1ilem  8053  findcard2  8059  isfinite2  8077  unfi  8086  fodomfib  8099  inf0  8375  rankxplim2  8600  scott0  8606  ficardom  8644  cardaleph  8769  dfac5  8808  cflim2  8942  fin23lem23  9005  fin23lem28  9019  isf32lem5  9036  domtriomlem  9121  ac6num  9158  zorn2lem5  9179  zorn2lem6  9180  iunfo  9214  axrepndlem2  9268  axregnd  9279  hargch  9348  addcanpi  9574  mulcanpi  9575  indpi  9582  ltaddnq  9649  ltexnq  9650  prlem934  9708  ltaddpr2  9710  ltaprlem  9719  supsrlem  9785  ssxr  9955  ltxrlt  9956  addcan  10068  addcan2  10069  neg11  10180  negreb  10194  mulcand  10506  receu  10518  lemul1a  10723  cju  10860  nn1suc  10885  nnaddcl  10886  nndivtr  10906  znegclb  11244  zmulcl  11256  zeo  11292  uz11  11539  uzp1  11550  eqreznegel  11603  rpnnen1lem6  11648  rpnnen1OLD  11654  xrltne  11826  xneg11  11876  xnegdi  11904  xrsupss  11964  xrinfmss  11965  elfznelfzob  12392  modadd1  12521  modmul1  12537  om2uzlti  12563  bccmpl  12910  hashen  12946  fz1eqb  12956  hashfn  12974  hashnn0n0nn  12990  hashtpg  13068  eqwrd  13144  ccatopth  13265  ccatopth2  13266  swrdccatin2  13281  swrdccat3a  13288  cj11  13693  rennim  13770  cnpart  13771  sqrmo  13783  sqrtgt0  13790  sqreulem  13890  sqreu  13891  lo1o1  14054  lo1eq  14090  rlimeq  14091  sumss  14245  cvgcmp  14332  fprodser  14461  efne0  14609  dvdsabseq  14816  divalglem8  14904  bitsinv1lem  14944  pcfac  15384  prmreclem3  15403  sectmon  16208  yoniso  16691  lublecllem  16754  oduposb  16902  mgmb1mgm1  17020  sgrp2rid2  17179  grpinveu  17222  mulgass  17345  galcan  17503  symg1bas  17582  cayleylem2  17599  odbezout  17741  odeq1  17743  dprddomcld  18166  dvreq1  18459  unitrrg  19057  coe1tm  19407  frgpcyg  19683  obslbs  19832  tgss3  20540  uptx  21177  txindislem  21185  qtopeu  21268  hmeocnvb  21326  qtophmeo  21369  trufil  21463  ufinffr  21482  ghmcnp  21667  tgioo  22336  lmmcvg  22782  bcth3  22850  ovolunlem1a  22985  vitali  23102  ismbf  23117  ismbfcn  23118  rolle  23471  itgsubstlem  23529  vieta1lem2  23784  elqaalem3  23794  aacjcl  23800  efif1olem4  24009  lognegb  24054  logcj  24070  argimgt0  24076  logdmnrp  24101  logcnlem3  24104  logrec  24215  dcubic  24287  isppw  24554  rplogsumlem2  24888  pntpbnd1  24989  axlowdimlem16  25552  nbgrassvwo2  25730  is2wlk  25858  wwlkn0  25980  wlkiswwlk1  25981  wlklniswwlkn1  25990  wlklniswwlkn2  25991  wwlksubclwwlk  26095  el2wlkonot  26159  frg2wot1  26347  grpoinveu  26520  grpoinvf  26533  diporthcom  26756  norm1exi  27294  shmodsi  27435  shmodi  27436  dfch2  27453  orthin  27492  chssoc  27542  spansncvi  27698  kbpj  28002  lnopunilem1  28056  cnlnssadj  28126  bra11  28154  strlem4  28300  strlem5  28301  hstrlem4  28308  hstrlem5  28309  dmdmd  28346  mdslle1i  28363  mdslle2i  28364  mdslmd1lem1  28371  atcvatlem  28431  atcvat4i  28443  mdsymlem3  28451  bcm1n  28744  xmulcand  28763  xreceu  28764  tpr2rico  29089  bnj1125  30117  mrsubff1  30468  mvhf1  30513  funpsstri  30712  sltres  30864  nofulllem1  30904  nofulllem2  30905  btwnintr  31099  idinside  31164  btwnconn1lem13  31179  fneval  31320  bj-sb4v  31751  bj-sbftv  31758  bj-equsal1t  31807  bj-ldiv  32132  bj-bary1lem1  32138  bj-bary1  32139  wl-equsal1i  32308  uncf  32358  matunitlindflem2  32376  poimirlem4  32383  poimirlem9  32388  ismtybndlem  32575  grpoeqdivid  32650  0rngo  32796  ax12indalem  33048  ax12inda2ALT  33049  lcvexchlem4  33142  lcvexchlem5  33143  opcon3b  33301  2dim  33574  ps-1  33581  paddclN  33946  ltrnnid  34240  cdleme22b  34447  dihmeetlem13N  35426  dih1dimatlem  35436  dihlspsnat  35440  frege58c  37035  sscon34b  37137  gneispa  37248  nzss  37338  expgrowth  37356  sbiota1  37457  bgoldbwt  40001  usgr0vb  40462  nbgrssvwo2  40586  red1wlk  40880  usgr2pthspth  40967  usgr2pth  40969  1wlkpwwlkf1ouspgr  41075  1wlklnwwlkln2lem  41078  wwlksubclwwlks  41231  frgr0v  41432  frgr2wwlk1  41493  dignn0flhalflem1  42206  aacllem  42316
  Copyright terms: Public domain W3C validator