Theorem syl5ib 222

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 210	. 2 |- ( ch -> ( ps -> th ) )
4	1, 3	syl5 33	1 |- ( ch -> ( ph -> th ) )

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

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 188

This theorem is referenced by:  syl5ibcom  223  syl5ibr  224  dvelimdf  2130  sb4  2148  sbft  2171  gencl  3108  spsbc  3309  eqsbc3r  3353  ssnelpss  3854  uniintsn  4287  prex  4656  copsexg  4699  posn  4915  optocl  4923  ordtri3  5470  funimass1  5666  f1ocnvb  5836  eqfnfv2  5984  elpreima  6009  fconst5  6129  dff13  6166  f1ocnvfv  6184  f1ocnvfvb  6185  fliftfun  6212  eusvobj2  6290  sorpsscmpl  6588  ssonprc  6625  xpexr  6739  xpexcnv  6741  relcnvexb  6747  dmfex  6757  frxp  6909  mpt2xopn0yelv  6959  rntpos  6986  oawordeulem  7255  oalimcl  7261  odi  7280  omeulem2  7284  oeeulem  7302  erexb  7388  unxpdomlem2  7775  dif1en  7802  enp1ilem  7803  findcard2  7809  isfinite2  7827  unfi  7836  fodomfib  7849  inf0  8124  rankxplim2  8348  scott0  8354  ficardom  8392  cardaleph  8516  dfac5  8555  cflim2  8689  fin23lem23  8752  fin23lem28  8766  isf32lem5  8783  domtriomlem  8868  ac6num  8905  zorn2lem5  8926  zorn2lem6  8927  iunfo  8960  axrepndlem2  9014  axregnd  9025  hargch  9094  addcanpi  9320  mulcanpi  9321  indpi  9328  ltaddnq  9395  ltexnq  9396  prlem934  9454  ltaddpr2  9456  ltaprlem  9465  supsrlem  9531  ssxr  9699  ltxrlt  9700  addcan  9813  addcan2  9814  neg11  9921  negreb  9935  mulcand  10241  receu  10253  lemul1a  10455  cju  10601  nn1suc  10626  nnaddcl  10627  nndivtr  10647  znegclb  10970  zmulcl  10981  zeo  11017  uz11  11177  uzp1  11188  eqreznegel  11245  rpnnen1  11291  xrltne  11456  xneg11  11504  xnegdi  11530  xrsupss  11590  xrinfmss  11591  elfznelfzob  12008  modadd1  12127  modmul1  12136  om2uzlti  12157  bccmpl  12487  hashen  12523  fz1eqb  12529  hashfn  12547  hashnn0n0nn  12563  hashtpg  12628  eqwrd  12691  ccatopth  12807  ccatopth2  12808  swrdccatin2  12824  swrdccat3a  12831  cj11  13204  rennim  13281  cnpart  13282  sqrmo  13294  sqrtgt0  13301  sqreulem  13401  sqreu  13402  lo1o1  13574  lo1eq  13610  rlimeq  13611  sumss  13768  cvgcmp  13854  fprodser  13981  efne0  14129  dvdseq  14330  divalglem8  14358  bitsinv1lem  14393  pcfac  14822  prmreclem3  14840  sectmon  15665  yoniso  16148  lublecllem  16212  oduposb  16360  mgmb1mgm1  16477  sgrp2rid2  16638  grpinveu  16678  mulgass  16766  galcan  16936  symg1bas  17015  cayleylem2  17032  odbezout  17187  odeq1  17189  dprddomcld  17611  dvreq1  17899  unitrrg  18495  coe1tm  18844  frgpcyg  19121  obslbs  19270  tgss3  19979  uptx  20617  txindislem  20625  qtopeu  20708  hmeocnvb  20766  qtophmeo  20809  trufil  20902  ufinffr  20921  ghmcnp  21106  tgioo  21791  lmmcvg  22208  bcth3  22276  ovolunlem1a  22426  vitali  22548  ismbf  22563  ismbfcn  22564  rolle  22919  itgsubstlem  22977  vieta1lem2  23241  elqaalem3  23251  elqaalem3OLD  23254  aacjcl  23260  efif1olem4  23471  lognegb  23516  logcj  23532  argimgt0  23538  logdmnrp  23563  logcnlem3  23566  logrec  23677  dcubic  23749  isppw  24018  rplogsumlem2  24300  pntpbnd1  24401  axlowdimlem16  24964  nbgrassvwo2  25142  is2wlk  25271  wwlkn0  25393  wlkiswwlk1  25394  wlklniswwlkn1  25403  wlklniswwlkn2  25404  wwlksubclwwlk  25508  el2wlkonot  25573  frg2wot1  25761  grpoinveu  25926  grpoinvf  25944  diporthcom  26331  norm1exi  26879  shmodsi  27018  shmodi  27019  dfch2  27036  orthin  27075  chssoc  27125  spansncvi  27281  kbpj  27585  lnopunilem1  27639  cnlnssadj  27709  bra11  27737  strlem4  27883  strlem5  27884  hstrlem4  27891  hstrlem5  27892  dmdmd  27929  mdslle1i  27946  mdslle2i  27947  mdslmd1lem1  27954  atcvatlem  28014  atcvat4i  28026  mdsymlem3  28034  bcm1n  28356  xmulcand  28377  xreceu  28378  tpr2rico  28707  bnj1125  29790  mrsubff1  30141  mvhf1  30186  funpsstri  30394  sltres  30539  nofulllem1  30577  nofulllem2  30578  btwnintr  30772  idinside  30837  btwnconn1lem13  30852  fneval  30994  bj-sb4v  31318  bj-sbftv  31326  bj-equsal1t  31376  bj-ldiv  31656  bj-bary1lem1  31662  bj-bary1  31663  wl-equsal1i  31784  poimirlem4  31852  poimirlem9  31857  dvtanlemOLD  31899  ismtybndlem  32046  grpoeqdivid  32087  0rngo  32168  ax12indalem  32429  ax12inda2ALT  32430  lcvexchlem4  32516  lcvexchlem5  32517  opcon3b  32675  2dim  32948  ps-1  32955  paddclN  33320  ltrnnid  33614  cdleme22b  33821  dihmeetlem13N  34800  dih1dimatlem  34810  dihlspsnat  34814  frege58c  36369  nzss  36518  expgrowth  36536  sbiota1  36637  elmod2OLD  38346  bgoldbwt  38498  usgra2pth  38730  dignn0flhalflem1  39491  aacllem  39605