Theorem syl5ib 223

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

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

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 189

This theorem is referenced by:  syl5ibcom  224  syl5ibr  225  dvelimdf  2168  sb4  2186  sbft  2207  gencl  3076  spsbc  3279  eqsbc3r  3323  ssnelpss  3828  uniintsn  4271  prex  4641  copsexg  4686  posn  4902  optocl  4910  ordtri3  5458  funimass1  5654  f1ocnvb  5825  eqfnfv2  5975  elpreima  6000  fconst5  6120  dff13  6157  f1ocnvfv  6175  f1ocnvfvb  6176  fliftfun  6203  eusvobj2  6281  sorpsscmpl  6579  ssonprc  6616  xpexr  6730  xpexcnv  6732  relcnvexb  6738  dmfex  6748  frxp  6903  mpt2xopn0yelv  6956  rntpos  6983  oawordeulem  7252  oalimcl  7258  odi  7277  omeulem2  7281  oeeulem  7299  erexb  7385  unxpdomlem2  7774  dif1en  7801  enp1ilem  7802  findcard2  7808  isfinite2  7826  unfi  7835  fodomfib  7848  inf0  8123  rankxplim2  8348  scott0  8354  ficardom  8392  cardaleph  8517  dfac5  8556  cflim2  8690  fin23lem23  8753  fin23lem28  8767  isf32lem5  8784  domtriomlem  8869  ac6num  8906  zorn2lem5  8927  zorn2lem6  8928  iunfo  8961  axrepndlem2  9015  axregnd  9026  hargch  9095  addcanpi  9321  mulcanpi  9322  indpi  9329  ltaddnq  9396  ltexnq  9397  prlem934  9455  ltaddpr2  9457  ltaprlem  9466  supsrlem  9532  ssxr  9700  ltxrlt  9701  addcan  9814  addcan2  9815  neg11  9922  negreb  9936  mulcand  10242  receu  10254  lemul1a  10456  cju  10602  nn1suc  10627  nnaddcl  10628  nndivtr  10648  znegclb  10971  zmulcl  10982  zeo  11018  uz11  11178  uzp1  11189  eqreznegel  11246  rpnnen1  11292  xrltne  11457  xneg11  11505  xnegdi  11531  xrsupss  11591  xrinfmss  11592  elfznelfzob  12012  modadd1  12131  modmul1  12140  om2uzlti  12161  bccmpl  12491  hashen  12527  fz1eqb  12533  hashfn  12551  hashnn0n0nn  12567  hashtpg  12638  eqwrd  12705  ccatopth  12821  ccatopth2  12822  swrdccatin2  12838  swrdccat3a  12845  cj11  13218  rennim  13295  cnpart  13296  sqrmo  13308  sqrtgt0  13315  sqreulem  13415  sqreu  13416  lo1o1  13589  lo1eq  13625  rlimeq  13626  sumss  13783  cvgcmp  13869  fprodser  13996  efne0  14144  dvdseq  14345  divalglem8  14373  bitsinv1lem  14408  pcfac  14837  prmreclem3  14855  sectmon  15680  yoniso  16163  lublecllem  16227  oduposb  16375  mgmb1mgm1  16492  sgrp2rid2  16653  grpinveu  16693  mulgass  16781  galcan  16951  symg1bas  17030  cayleylem2  17047  odbezout  17202  odeq1  17204  dprddomcld  17626  dvreq1  17914  unitrrg  18510  coe1tm  18859  frgpcyg  19137  obslbs  19286  tgss3  19995  uptx  20633  txindislem  20641  qtopeu  20724  hmeocnvb  20782  qtophmeo  20825  trufil  20918  ufinffr  20937  ghmcnp  21122  tgioo  21807  lmmcvg  22224  bcth3  22292  ovolunlem1a  22442  vitali  22564  ismbf  22579  ismbfcn  22580  rolle  22935  itgsubstlem  22993  vieta1lem2  23257  elqaalem3  23267  elqaalem3OLD  23270  aacjcl  23276  efif1olem4  23487  lognegb  23532  logcj  23548  argimgt0  23554  logdmnrp  23579  logcnlem3  23582  logrec  23693  dcubic  23765  isppw  24034  rplogsumlem2  24316  pntpbnd1  24417  axlowdimlem16  24980  nbgrassvwo2  25159  is2wlk  25288  wwlkn0  25410  wlkiswwlk1  25411  wlklniswwlkn1  25420  wlklniswwlkn2  25421  wwlksubclwwlk  25525  el2wlkonot  25590  frg2wot1  25778  grpoinveu  25943  grpoinvf  25961  diporthcom  26348  norm1exi  26896  shmodsi  27035  shmodi  27036  dfch2  27053  orthin  27092  chssoc  27142  spansncvi  27298  kbpj  27602  lnopunilem1  27656  cnlnssadj  27726  bra11  27754  strlem4  27900  strlem5  27901  hstrlem4  27908  hstrlem5  27909  dmdmd  27946  mdslle1i  27963  mdslle2i  27964  mdslmd1lem1  27971  atcvatlem  28031  atcvat4i  28043  mdsymlem3  28051  bcm1n  28364  xmulcand  28383  xreceu  28384  tpr2rico  28711  bnj1125  29794  mrsubff1  30145  mvhf1  30190  funpsstri  30399  sltres  30544  nofulllem1  30584  nofulllem2  30585  btwnintr  30779  idinside  30844  btwnconn1lem13  30859  fneval  31001  bj-sb4v  31362  bj-sbftv  31369  bj-equsal1t  31417  bj-ldiv  31703  bj-bary1lem1  31709  bj-bary1  31710  wl-equsal1i  31869  poimirlem4  31937  poimirlem9  31942  dvtanlemOLD  31984  ismtybndlem  32131  grpoeqdivid  32172  0rngo  32253  ax12indalem  32510  ax12inda2ALT  32511  lcvexchlem4  32597  lcvexchlem5  32598  opcon3b  32756  2dim  33029  ps-1  33036  paddclN  33401  ltrnnid  33695  cdleme22b  33902  dihmeetlem13N  34881  dih1dimatlem  34891  dihlspsnat  34895  frege58c  36511  nzss  36660  expgrowth  36678  sbiota1  36779  elmod2OLD  38720  bgoldbwt  38872  usgr0vb  39299  nbgrssvwo2  39416  usgra2pth  39655  dignn0flhalflem1  40413  aacllem  40527