Theorem syl5ib 219

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

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 32	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  2026  sb4  2046  sbft  2067  ax12indalem  2247  ax12inda2ALT  2248  gencl  2991  spsbc  3187  eqsbc3r  3236  ssnelpss  3730  uniintsn  4153  prex  4522  ordtri3  4742  posn  4894  optocl  4900  funimass1  5479  f1ocnvb  5642  eqfnfv2  5786  elpreima  5811  fconst5  5922  dff13  5958  f1ocnvfv  5972  f1ocnvfvb  5973  fliftfun  5992  eusvobj2  6072  sorpsscmpl  6360  ssonprc  6392  xpexr  6507  xpexcnv  6509  relcnvexb  6515  dmfex  6524  frxp  6671  mpt2xopn0yelv  6719  rntpos  6747  oawordeulem  6981  oalimcl  6987  odi  7006  omeulem2  7010  oeeulem  7028  erexb  7114  unxpdomlem2  7506  dif1enOLD  7532  dif1en  7533  enp1ilem  7534  findcard2  7540  isfinite2  7558  unfi  7567  fodomfib  7579  inf0  7815  rankxplim2  8075  scott0  8081  ficardom  8119  cardaleph  8247  dfac5  8286  cflim2  8420  fin23lem23  8483  fin23lem28  8497  isf32lem5  8514  domtriomlem  8599  ac6num  8636  zorn2lem5  8657  zorn2lem6  8658  iunfo  8691  axrepndlem2  8745  axregnd  8758  hargch  8827  addcanpi  9055  mulcanpi  9056  indpi  9063  ltaddnq  9130  ltexnq  9131  prlem934  9189  ltaddpr2  9191  ltaprlem  9200  supsrlem  9265  ssxr  9431  ltxrlt  9432  addcan  9540  addcan2  9541  neg11  9647  negreb  9661  mulcand  9956  receu  9968  lemul1a  10170  cju  10305  nn1suc  10330  nnaddcl  10331  nndivtr  10350  znegclb  10669  zmulcl  10680  zeo  10714  uz11  10870  uzp1  10881  eqreznegel  10927  rpnnen1  10971  xrltne  11124  xneg11  11172  xnegdi  11198  xrsupss  11258  xrinfmss  11259  elfznelfzob  11614  modadd1  11728  modmul1  11735  om2uzlti  11756  bccmpl  12068  hashen  12101  fz1eqb  12107  hashfn  12121  hashnn0n0nn  12136  hashtpg  12169  eqwrd  12248  ccatopth  12347  ccatopth2  12348  swrdccatin2  12361  swrdccat3a  12368  cj11  12634  rennim  12711  cnpart  12712  sqrmo  12724  sqrgt0  12731  sqreulem  12830  sqreu  12831  lo1o1  12993  lo1eq  13029  rlimeq  13030  sumss  13184  cvgcmp  13261  efne0  13363  dvdseq  13562  divalglem8  13586  bitsinv1lem  13619  pcfac  13943  prmreclem3  13961  sectmon  14698  yoniso  15077  lublecllem  15140  oduposb  15288  grpinveu  15551  mulgass  15636  galcan  15801  symg1bas  15880  cayleylem2  15897  odbezout  16038  odeq1  16040  dprddomcld  16456  dvreq1  16718  unitrrg  17286  coe1tm  17623  frgpcyg  17847  obslbs  17996  tgss3  18432  uptx  19039  txindislem  19047  qtopeu  19130  hmeocnvb  19188  qtophmeo  19231  trufil  19324  ufinffr  19343  ghmcnp  19526  tgioo  20214  lmmcvg  20613  bcth3  20683  ovolunlem1a  20820  vitali  20934  ismbf  20949  ismbfcn  20950  rolle  21303  itgsubstlem  21361  vieta1lem2  21661  elqaalem3  21671  aacjcl  21677  efif1olem4  21885  lognegb  21922  logcj  21939  argimgt0  21945  logdmnrp  21970  logcnlem3  21973  logrec  22099  dcubic  22125  isppw  22336  rplogsumlem2  22618  pntpbnd1  22719  axlowdimlem16  23025  is2wlk  23286  grpoinveu  23531  grpoinvf  23549  diporthcom  23936  norm1exi  24475  shmodsi  24614  shmodi  24615  dfch2  24632  orthin  24671  chssoc  24721  spansncvi  24877  kbpj  25182  lnopunilem1  25236  cnlnssadj  25306  bra11  25334  strlem4  25480  strlem5  25481  hstrlem4  25488  hstrlem5  25489  dmdmd  25526  mdslle1i  25543  mdslle2i  25544  mdslmd1lem1  25551  atcvatlem  25611  atcvat4i  25623  mdsymlem3  25631  bcm1n  25901  xmulcand  25918  xreceu  25919  tpr2rico  26195  fprodser  27308  funpsstri  27422  sltres  27651  nofulllem1  27689  nofulllem2  27690  btwnintr  27896  idinside  27961  btwnconn1lem13  27976  wl-equsal1i  28218  dvtanlem  28282  fneval  28400  ismtybndlem  28546  grpoeqdivid  28587  0rngo  28668  expgrowth  29451  sbiota1  29530  nbgrassvwo2  30120  usgra2pth  30144  wwlkn0  30166  wlkiswwlk1  30167  wlklniswwlkn1  30176  wlklniswwlkn2  30177  el2wlkonot  30231  wwlksubclwwlk  30309  frg2wot1  30493  bnj1125  31682  bj-sb4v  31899  bj-sbftv  31904  bj-equsal1t  31947  bj-ldiv  32166  bj-bary1lem1  32172  bj-bary1  32173  lcvexchlem4  32252  lcvexchlem5  32253  opcon3b  32411  2dim  32684  ps-1  32691  paddclN  33056  ltrnnid  33350  cdleme22b  33555  dihmeetlem13N  34534  dih1dimatlem  34544  dihlspsnat  34548