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

Theorem syl5ib 210
Description: A mixed syllogism inference. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5ib.1  |-  ( ph  ->  ps )
syl5ib.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5ib  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem syl5ib
StepHypRef Expression
1 syl5ib.1 . 2  |-  ( ph  ->  ps )
2 syl5ib.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
32biimpd 198 . 2  |-  ( ch 
->  ( ps  ->  th )
)
41, 3syl5 28 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  syl5ibcom  211  syl5ibr  212  19.23t  1796  nfsb4t  2020  ax11indalem  2136  ax11inda2ALT  2137  gencl  2816  spsbc  3003  eqsbc3r  3048  ssnelpss  3517  uniintsn  3899  prex  4217  ordtri3  4428  ssonprc  4583  posn  4758  optocl  4764  xpexr  5114  relcnvexb  5210  funimass1  5325  dmfex  5424  f1ocnvb  5486  eqfnfv2  5623  elpreima  5645  fconst5  5731  dff13  5783  f1ocnvfv  5794  f1ocnvfvb  5795  fliftfun  5811  frxp  6225  rntpos  6247  sorpsscmpl  6288  eusvobj2  6337  oawordeulem  6552  oalimcl  6558  odi  6577  omeulem2  6581  oeeulem  6599  erexb  6685  unxpdomlem2  7068  dif1enOLD  7090  dif1en  7091  enp1ilem  7092  findcard2  7098  isfinite2  7115  unfi  7124  fodomfib  7136  inf0  7322  rankxplim2  7550  scott0  7556  ficardom  7594  cardaleph  7716  dfac5  7755  cflim2  7889  fin23lem23  7952  fin23lem28  7966  isf32lem5  7983  domtriomlem  8068  ac6num  8106  zorn2lem5  8127  zorn2lem6  8128  iunfo  8161  axrepndlem2  8215  axregnd  8226  hargch  8299  addcanpi  8523  mulcanpi  8524  indpi  8531  ltaddnq  8598  ltexnq  8599  prlem934  8657  ltaddpr2  8659  ltaprlem  8668  supsrlem  8733  ssxr  8892  ltxrlt  8893  addcan  8996  addcan2  8997  neg11  9098  negreb  9112  mulcand  9401  receu  9413  lemul1a  9610  cju  9742  nn1suc  9767  nnaddcl  9768  nndivtr  9787  znegclb  10056  zmulcl  10066  zeo  10097  uz11  10250  uzp1  10261  eqreznegel  10303  rpnnen1  10347  xrltne  10494  xneg11  10542  xnegdi  10568  xrsupss  10627  xrinfmss  10628  modadd1  11001  modmul1  11002  om2uzlti  11013  bccmpl  11322  hashen  11346  fz1eqb  11348  hashfn  11357  ccatopth  11462  ccatopth2  11463  cj11  11647  rennim  11724  cnpart  11725  sqrmo  11737  sqrgt0  11744  sqreulem  11843  sqreu  11844  lo1o1  12006  lo1eq  12042  rlimeq  12043  sumss  12197  cvgcmp  12274  efne0  12377  dvdseq  12576  divalglem8  12599  bitsinv1lem  12632  pcfac  12947  prmreclem3  12965  sectmon  13680  yoniso  14059  lubid  14116  oduposb  14240  grpinveu  14516  mulgass  14597  galcan  14758  cayleylem2  14788  odbezout  14871  odeq1  14873  dvreq1  15475  unitrrg  16034  coe1tm  16349  frgpcyg  16527  obslbs  16630  tgss3  16724  uptx  17319  txindislem  17327  qtopeu  17407  hmeocnvb  17465  qtophmeo  17508  trufil  17605  ufinffr  17624  ghmcnp  17797  tgioo  18302  lmmcvg  18687  bcth3  18753  ovolunlem1a  18855  vitali  18968  ismbf  18985  ismbfcn  18986  rolle  19337  itgsubstlem  19395  vieta1lem2  19691  elqaalem3  19701  aacjcl  19707  efif1olem4  19907  lognegb  19943  logcj  19960  argimgt0  19966  logdmnrp  19988  logcnlem3  19991  logrec  20117  dcubic  20142  isppw  20352  rplogsumlem2  20634  pntpbnd1  20735  grpoinveu  20889  grpoinvf  20907  diporthcom  21292  norm1exi  21829  shmodsi  21968  shmodi  21969  dfch2  21986  orthin  22025  chssoc  22075  spansncvi  22231  kbpj  22536  lnopunilem1  22590  cnlnssadj  22660  bra11  22688  strlem4  22834  strlem5  22835  hstrlem4  22842  hstrlem5  22843  dmdmd  22880  mdslle1i  22897  mdslle2i  22898  mdslmd1lem1  22905  atcvatlem  22965  atcvat4i  22977  mdsymlem3  22985  bcm1n  23032  funpsstri  23532  sltres  23729  nofulllem1  23767  nofulllem2  23768  axlowdimlem16  23996  btwnintr  24053  idinside  24118  btwnconn1lem13  24133  svs3  24900  1ded  25150  1cat  25171  fneval  25699  ismtybndlem  25942  grpoeqdivid  25983  0rngo  26064  expgrowth  26964  sbiota1  27046  xpexcnv  27071  bnj1125  28395  lcvexchlem4  28600  lcvexchlem5  28601  opcon3b  28759  2dim  29032  ps-1  29039  paddclN  29404  ltrnnid  29698  cdleme22b  29903  dihmeetlem13N  30882  dih1dimatlem  30892  dihlspsnat  30896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator