Theorem syl5ib 219

Description: A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.)

Hypotheses

Ref	Expression
syl5ib.1	|- ( ph -> ps )
syl5ib.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
syl5ib	|- ( ch -> ( ph -> th ) )

Proof of Theorem syl5ib

Step	Hyp	Ref	Expression
1		syl5ib.1	. 2 |- ( ph -> ps )
2		syl5ib.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	2	biimpd 207	. 2 |- ( ch -> ( ps -> th ) )
4	1, 3	syl5 30	1 |- ( ch -> ( ph -> th ) )

Syntax hints:   -> wi 4   <-> wb 184

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 185

This theorem is referenced by:  syl5ibcom  220  syl5ibr  221  dvelimdf  2103  sb4  2121  sbft  2144  gencl  3088  spsbc  3289  eqsbc3r  3333  ssnelpss  3833  uniintsn  4264  prex  4632  copsexg  4675  posn  4891  optocl  4899  ordtri3  5445  funimass1  5641  f1ocnvb  5811  eqfnfv2  5959  elpreima  5984  fconst5  6108  dff13  6146  f1ocnvfv  6164  f1ocnvfvb  6165  fliftfun  6192  eusvobj2  6270  sorpsscmpl  6572  ssonprc  6609  xpexr  6723  xpexcnv  6725  relcnvexb  6731  dmfex  6741  frxp  6893  mpt2xopn0yelv  6943  rntpos  6970  oawordeulem  7239  oalimcl  7245  odi  7264  omeulem2  7268  oeeulem  7286  erexb  7372  unxpdomlem2  7759  dif1en  7786  enp1ilem  7787  findcard2  7793  isfinite2  7811  unfi  7820  fodomfib  7833  inf0  8070  rankxplim2  8329  scott0  8335  ficardom  8373  cardaleph  8501  dfac5  8540  cflim2  8674  fin23lem23  8737  fin23lem28  8751  isf32lem5  8768  domtriomlem  8853  ac6num  8890  zorn2lem5  8911  zorn2lem6  8912  iunfo  8945  axrepndlem2  8999  axregnd  9010  axregndOLD  9011  hargch  9080  addcanpi  9306  mulcanpi  9307  indpi  9314  ltaddnq  9381  ltexnq  9382  prlem934  9440  ltaddpr2  9442  ltaprlem  9451  supsrlem  9517  ssxr  9684  ltxrlt  9685  addcan  9797  addcan2  9798  neg11  9905  negreb  9919  mulcand  10222  receu  10234  lemul1a  10436  cju  10571  nn1suc  10596  nnaddcl  10597  nndivtr  10617  znegclb  10941  zmulcl  10952  zeo  10988  uz11  11148  uzp1  11159  eqreznegel  11211  rpnnen1  11257  xrltne  11418  xneg11  11466  xnegdi  11492  xrsupss  11552  xrinfmss  11553  elfznelfzob  11951  modadd1  12070  modmul1  12079  om2uzlti  12100  bccmpl  12429  hashen  12465  fz1eqb  12471  hashfn  12489  hashnn0n0nn  12505  hashtpg  12570  eqwrd  12633  ccatopth  12749  ccatopth2  12750  swrdccatin2  12766  swrdccat3a  12773  cj11  13142  rennim  13219  cnpart  13220  sqrmo  13232  sqrtgt0  13239  sqreulem  13339  sqreu  13340  lo1o1  13502  lo1eq  13538  rlimeq  13539  sumss  13693  cvgcmp  13779  fprodser  13906  efne0  14039  dvdseq  14240  divalglem8  14265  bitsinv1lem  14298  pcfac  14625  prmreclem3  14643  sectmon  15393  yoniso  15876  lublecllem  15940  oduposb  16088  mgmb1mgm1  16205  sgrp2rid2  16366  grpinveu  16406  mulgass  16494  galcan  16664  symg1bas  16743  cayleylem2  16760  odbezout  16902  odeq1  16904  dprddomcld  17350  dvreq1  17660  unitrrg  18260  coe1tm  18632  frgpcyg  18908  obslbs  19057  tgss3  19778  uptx  20416  txindislem  20424  qtopeu  20507  hmeocnvb  20565  qtophmeo  20608  trufil  20701  ufinffr  20720  ghmcnp  20903  tgioo  21591  lmmcvg  21990  bcth3  22060  ovolunlem1a  22197  vitali  22312  ismbf  22327  ismbfcn  22328  rolle  22681  itgsubstlem  22739  vieta1lem2  22997  elqaalem3  23007  aacjcl  23013  efif1olem4  23222  lognegb  23267  logcj  23283  argimgt0  23289  logdmnrp  23314  logcnlem3  23317  logrec  23428  dcubic  23500  isppw  23767  rplogsumlem2  24049  pntpbnd1  24150  axlowdimlem16  24664  nbgrassvwo2  24842  is2wlk  24971  wwlkn0  25093  wlkiswwlk1  25094  wlklniswwlkn1  25103  wlklniswwlkn2  25104  wwlksubclwwlk  25208  el2wlkonot  25273  frg2wot1  25461  grpoinveu  25624  grpoinvf  25642  diporthcom  26029  norm1exi  26568  shmodsi  26707  shmodi  26708  dfch2  26725  orthin  26764  chssoc  26814  spansncvi  26970  kbpj  27274  lnopunilem1  27328  cnlnssadj  27398  bra11  27426  strlem4  27572  strlem5  27573  hstrlem4  27580  hstrlem5  27581  dmdmd  27618  mdslle1i  27635  mdslle2i  27636  mdslmd1lem1  27643  atcvatlem  27703  atcvat4i  27715  mdsymlem3  27723  bcm1n  28034  xmulcand  28055  xreceu  28056  tpr2rico  28333  bnj1125  29362  mrsubff1  29713  mvhf1  29758  funpsstri  29966  sltres  30111  nofulllem1  30149  nofulllem2  30150  btwnintr  30344  idinside  30409  btwnconn1lem13  30424  fneval  30567  bj-sb4v  30888  bj-sbftv  30896  bj-equsal1t  30946  bj-ldiv  31222  bj-bary1lem1  31228  bj-bary1  31229  wl-equsal1i  31348  dvtanlemOLD  31417  ismtybndlem  31564  grpoeqdivid  31605  0rngo  31686  ax12indalem  31948  ax12inda2ALT  31949  lcvexchlem4  32035  lcvexchlem5  32036  opcon3b  32194  2dim  32467  ps-1  32474  paddclN  32839  ltrnnid  33133  cdleme22b  33340  dihmeetlem13N  34319  dih1dimatlem  34329  dihlspsnat  34333  frege58c  35882  nzss  36050  expgrowth  36068  sbiota1  36169  elmod2OLD  37658  bgoldbwt  37812  usgra2pth  37964  dignn0flhalflem1  38727  aacllem  38841