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  1808  nfsb4t  2033  ax11indalem  2149  ax11inda2ALT  2150  gencl  2829  spsbc  3016  eqsbc3r  3061  ssnelpss  3530  uniintsn  3915  prex  4233  ordtri3  4444  ssonprc  4599  posn  4774  optocl  4780  xpexr  5130  relcnvexb  5226  funimass1  5341  dmfex  5440  f1ocnvb  5502  eqfnfv2  5639  elpreima  5661  fconst5  5747  dff13  5799  f1ocnvfv  5810  f1ocnvfvb  5811  fliftfun  5827  frxp  6241  rntpos  6263  sorpsscmpl  6304  eusvobj2  6353  oawordeulem  6568  oalimcl  6574  odi  6593  omeulem2  6597  oeeulem  6615  erexb  6701  unxpdomlem2  7084  dif1enOLD  7106  dif1en  7107  enp1ilem  7108  findcard2  7114  isfinite2  7131  unfi  7140  fodomfib  7152  inf0  7338  rankxplim2  7566  scott0  7572  ficardom  7610  cardaleph  7732  dfac5  7771  cflim2  7905  fin23lem23  7968  fin23lem28  7982  isf32lem5  7999  domtriomlem  8084  ac6num  8122  zorn2lem5  8143  zorn2lem6  8144  iunfo  8177  axrepndlem2  8231  axregnd  8242  hargch  8315  addcanpi  8539  mulcanpi  8540  indpi  8547  ltaddnq  8614  ltexnq  8615  prlem934  8673  ltaddpr2  8675  ltaprlem  8684  supsrlem  8749  ssxr  8908  ltxrlt  8909  addcan  9012  addcan2  9013  neg11  9114  negreb  9128  mulcand  9417  receu  9429  lemul1a  9626  cju  9758  nn1suc  9783  nnaddcl  9784  nndivtr  9803  znegclb  10072  zmulcl  10082  zeo  10113  uz11  10266  uzp1  10277  eqreznegel  10319  rpnnen1  10363  xrltne  10510  xneg11  10558  xnegdi  10584  xrsupss  10643  xrinfmss  10644  modadd1  11017  modmul1  11018  om2uzlti  11029  bccmpl  11338  hashen  11362  fz1eqb  11364  hashfn  11373  ccatopth  11478  ccatopth2  11479  cj11  11663  rennim  11740  cnpart  11741  sqrmo  11753  sqrgt0  11760  sqreulem  11859  sqreu  11860  lo1o1  12022  lo1eq  12058  rlimeq  12059  sumss  12213  cvgcmp  12290  efne0  12393  dvdseq  12592  divalglem8  12615  bitsinv1lem  12648  pcfac  12963  prmreclem3  12981  sectmon  13696  yoniso  14075  lubid  14132  oduposb  14256  grpinveu  14532  mulgass  14613  galcan  14774  cayleylem2  14804  odbezout  14887  odeq1  14889  dvreq1  15491  unitrrg  16050  coe1tm  16365  frgpcyg  16543  obslbs  16646  tgss3  16740  uptx  17335  txindislem  17343  qtopeu  17423  hmeocnvb  17481  qtophmeo  17524  trufil  17621  ufinffr  17640  ghmcnp  17813  tgioo  18318  lmmcvg  18703  bcth3  18769  ovolunlem1a  18871  vitali  18984  ismbf  19001  ismbfcn  19002  rolle  19353  itgsubstlem  19411  vieta1lem2  19707  elqaalem3  19717  aacjcl  19723  efif1olem4  19923  lognegb  19959  logcj  19976  argimgt0  19982  logdmnrp  20004  logcnlem3  20007  logrec  20133  dcubic  20158  isppw  20368  rplogsumlem2  20650  pntpbnd1  20751  grpoinveu  20905  grpoinvf  20923  diporthcom  21308  norm1exi  21845  shmodsi  21984  shmodi  21985  dfch2  22002  orthin  22041  chssoc  22091  spansncvi  22247  kbpj  22552  lnopunilem1  22606  cnlnssadj  22676  bra11  22704  strlem4  22850  strlem5  22851  hstrlem4  22858  hstrlem5  22859  dmdmd  22896  mdslle1i  22913  mdslle2i  22914  mdslmd1lem1  22921  atcvatlem  22981  atcvat4i  22993  mdsymlem3  23001  bcm1n  23048  xmulcand  23120  xreceu  23121  funpsstri  24192  sltres  24389  nofulllem1  24427  nofulllem2  24428  axlowdimlem16  24657  btwnintr  24714  idinside  24779  btwnconn1lem13  24794  svs3  25591  1ded  25841  1cat  25862  fneval  26390  ismtybndlem  26633  grpoeqdivid  26674  0rngo  26755  expgrowth  27655  sbiota1  27737  xpexcnv  27762  mpt2xopn0yelv  28195  hashtpg  28217  nbgrael  28275  bnj1125  29338  nfsb4twAUX7  29551  nfsb4tOLD7  29699  nfsb4tw2AUXOLD7  29700  lcvexchlem4  29849  lcvexchlem5  29850  opcon3b  30008  2dim  30281  ps-1  30288  paddclN  30653  ltrnnid  30947  cdleme22b  31152  dihmeetlem13N  32131  dih1dimatlem  32141  dihlspsnat  32145
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