Theorem syl5ib 227

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

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

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 190

This theorem is referenced by:  syl5ibcom  228  syl5ibr  229  dvelimdf  2184  sb4  2205  sbft  2228  gencl  3063  spsbc  3268  eqsbc3r  3312  ssnelpss  3530  uniintsn  4263  prex  4642  copsexg  4687  posn  4908  optocl  4916  ordtri3  5466  funimass1  5666  f1ocnvb  5841  eqfnfv2  5992  elpreima  6017  fconst5  6138  dff13  6177  f1ocnvfv  6195  f1ocnvfvb  6196  fliftfun  6223  eusvobj2  6301  sorpsscmpl  6601  ssonprc  6638  xpexr  6752  xpexcnv  6754  relcnvexb  6760  dmfex  6770  frxp  6925  mpt2xopn0yelv  6978  rntpos  7004  oawordeulem  7273  oalimcl  7279  odi  7298  omeulem2  7302  oeeulem  7320  erexb  7406  unxpdomlem2  7795  dif1en  7822  enp1ilem  7823  findcard2  7829  isfinite2  7847  unfi  7856  fodomfib  7869  inf0  8144  rankxplim2  8369  scott0  8375  ficardom  8413  cardaleph  8538  dfac5  8577  cflim2  8711  fin23lem23  8774  fin23lem28  8788  isf32lem5  8805  domtriomlem  8890  ac6num  8927  zorn2lem5  8948  zorn2lem6  8949  iunfo  8982  axrepndlem2  9036  axregnd  9047  hargch  9116  addcanpi  9342  mulcanpi  9343  indpi  9350  ltaddnq  9417  ltexnq  9418  prlem934  9476  ltaddpr2  9478  ltaprlem  9487  supsrlem  9553  ssxr  9721  ltxrlt  9722  addcan  9835  addcan2  9836  neg11  9945  negreb  9959  mulcand  10267  receu  10279  lemul1a  10481  cju  10627  nn1suc  10652  nnaddcl  10653  nndivtr  10673  znegclb  10998  zmulcl  11009  zeo  11044  uz11  11205  uzp1  11216  eqreznegel  11272  rpnnen1  11318  xrltne  11483  xneg11  11531  xnegdi  11559  xrsupss  11619  xrinfmss  11620  elfznelfzob  12046  modadd1  12167  modmul1  12177  om2uzlti  12202  bccmpl  12532  hashen  12568  fz1eqb  12574  hashfn  12592  hashnn0n0nn  12608  hashtpg  12682  eqwrd  12759  ccatopth  12880  ccatopth2  12881  swrdccatin2  12897  swrdccat3a  12904  cj11  13302  rennim  13379  cnpart  13380  sqrmo  13392  sqrtgt0  13399  sqreulem  13499  sqreu  13500  lo1o1  13673  lo1eq  13709  rlimeq  13710  sumss  13867  cvgcmp  13953  fprodser  14080  efne0  14228  dvdseq  14429  divalglem8  14459  bitsinv1lem  14494  pcfac  14923  prmreclem3  14941  sectmon  15765  yoniso  16248  lublecllem  16312  oduposb  16460  mgmb1mgm1  16577  sgrp2rid2  16738  grpinveu  16778  mulgass  16866  galcan  17036  symg1bas  17115  cayleylem2  17132  odbezout  17287  odeq1  17289  dprddomcld  17711  dvreq1  17999  unitrrg  18594  coe1tm  18943  frgpcyg  19221  obslbs  19370  tgss3  20079  uptx  20717  txindislem  20725  qtopeu  20808  hmeocnvb  20866  qtophmeo  20909  trufil  21003  ufinffr  21022  ghmcnp  21207  tgioo  21892  lmmcvg  22309  bcth3  22377  ovolunlem1a  22527  vitali  22650  ismbf  22665  ismbfcn  22666  rolle  23021  itgsubstlem  23079  vieta1lem2  23343  elqaalem3  23353  elqaalem3OLD  23356  aacjcl  23362  efif1olem4  23573  lognegb  23618  logcj  23634  argimgt0  23640  logdmnrp  23665  logcnlem3  23668  logrec  23779  dcubic  23851  isppw  24120  rplogsumlem2  24402  pntpbnd1  24503  axlowdimlem16  25066  nbgrassvwo2  25245  is2wlk  25374  wwlkn0  25496  wlkiswwlk1  25497  wlklniswwlkn1  25506  wlklniswwlkn2  25507  wwlksubclwwlk  25611  el2wlkonot  25676  frg2wot1  25864  grpoinveu  26031  grpoinvf  26049  diporthcom  26436  norm1exi  26984  shmodsi  27123  shmodi  27124  dfch2  27141  orthin  27180  chssoc  27230  spansncvi  27386  kbpj  27690  lnopunilem1  27744  cnlnssadj  27814  bra11  27842  strlem4  27988  strlem5  27989  hstrlem4  27996  hstrlem5  27997  dmdmd  28034  mdslle1i  28051  mdslle2i  28052  mdslmd1lem1  28059  atcvatlem  28119  atcvat4i  28131  mdsymlem3  28139  bcm1n  28446  xmulcand  28465  xreceu  28466  tpr2rico  28792  bnj1125  29873  mrsubff1  30224  mvhf1  30269  funpsstri  30477  sltres  30622  nofulllem1  30662  nofulllem2  30663  btwnintr  30857  idinside  30922  btwnconn1lem13  30937  fneval  31079  bj-sb4v  31435  bj-sbftv  31442  bj-equsal1t  31490  bj-ldiv  31780  bj-bary1lem1  31786  bj-bary1  31787  wl-equsal1i  31946  poimirlem4  32008  poimirlem9  32013  dvtanlemOLD  32055  ismtybndlem  32202  grpoeqdivid  32243  0rngo  32324  ax12indalem  32580  ax12inda2ALT  32581  lcvexchlem4  32674  lcvexchlem5  32675  opcon3b  32833  2dim  33106  ps-1  33113  paddclN  33478  ltrnnid  33772  cdleme22b  33979  dihmeetlem13N  34958  dih1dimatlem  34968  dihlspsnat  34972  frege58c  36588  nzss  36736  expgrowth  36754  sbiota1  36855  elmod2OLD  38871  bgoldbwt  39023  usgr0vb  39477  nbgrssvwo2  39597  usgra2pth  40176  dignn0flhalflem1  40934  aacllem  41046