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 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  2063  sb4  2083  sbft  2106  ax12indalem  2261  ax12inda2ALT  2262  gencl  3125  spsbc  3326  eqsbc3r  3375  ssnelpss  3876  uniintsn  4309  prex  4679  copsexg  4722  ordtri3  4904  posn  5058  optocl  5066  funimass1  5651  f1ocnvb  5819  eqfnfv2  5967  elpreima  5992  fconst5  6113  dff13  6151  f1ocnvfv  6169  f1ocnvfvb  6170  fliftfun  6195  eusvobj2  6274  sorpsscmpl  6576  ssonprc  6612  xpexr  6725  xpexcnv  6727  relcnvexb  6733  dmfex  6743  frxp  6895  mpt2xopn0yelv  6943  rntpos  6970  oawordeulem  7205  oalimcl  7211  odi  7230  omeulem2  7234  oeeulem  7252  erexb  7338  unxpdomlem2  7727  dif1enOLD  7754  dif1en  7755  enp1ilem  7756  findcard2  7762  isfinite2  7780  unfi  7789  fodomfib  7802  inf0  8041  rankxplim2  8301  scott0  8307  ficardom  8345  cardaleph  8473  dfac5  8512  cflim2  8646  fin23lem23  8709  fin23lem28  8723  isf32lem5  8740  domtriomlem  8825  ac6num  8862  zorn2lem5  8883  zorn2lem6  8884  iunfo  8917  axrepndlem2  8971  axregnd  8984  axregndOLD  8985  hargch  9054  addcanpi  9280  mulcanpi  9281  indpi  9288  ltaddnq  9355  ltexnq  9356  prlem934  9414  ltaddpr2  9416  ltaprlem  9425  supsrlem  9491  ssxr  9657  ltxrlt  9658  addcan  9767  addcan2  9768  neg11  9875  negreb  9889  mulcand  10189  receu  10201  lemul1a  10403  cju  10539  nn1suc  10564  nnaddcl  10565  nndivtr  10584  znegclb  10908  zmulcl  10919  zeo  10955  uz11  11113  uzp1  11124  eqreznegel  11177  rpnnen1  11223  xrltne  11376  xneg11  11424  xnegdi  11450  xrsupss  11510  xrinfmss  11511  elfznelfzob  11897  modadd1  12014  modmul1  12021  om2uzlti  12042  bccmpl  12368  hashen  12401  fz1eqb  12407  hashfn  12424  hashnn0n0nn  12439  hashtpg  12504  eqwrd  12563  ccatopth  12676  ccatopth2  12677  swrdccatin2  12693  swrdccat3a  12700  cj11  12976  rennim  13053  cnpart  13054  sqrmo  13066  sqrtgt0  13073  sqreulem  13173  sqreu  13174  lo1o1  13336  lo1eq  13372  rlimeq  13373  sumss  13527  cvgcmp  13611  fprodser  13737  efne0  13813  dvdseq  14014  divalglem8  14039  bitsinv1lem  14072  pcfac  14399  prmreclem3  14417  sectmon  15153  yoniso  15532  lublecllem  15596  oduposb  15744  mgmb1mgm1  15861  sgrp2rid2  16022  grpinveu  16062  mulgass  16150  galcan  16320  symg1bas  16399  cayleylem2  16416  odbezout  16558  odeq1  16560  dprddomcld  17010  dvreq1  17320  unitrrg  17920  coe1tm  18292  frgpcyg  18589  obslbs  18738  tgss3  19465  uptx  20103  txindislem  20111  qtopeu  20194  hmeocnvb  20252  qtophmeo  20295  trufil  20388  ufinffr  20407  ghmcnp  20590  tgioo  21278  lmmcvg  21677  bcth3  21747  ovolunlem1a  21884  vitali  21999  ismbf  22014  ismbfcn  22015  rolle  22368  itgsubstlem  22426  vieta1lem2  22683  elqaalem3  22693  aacjcl  22699  efif1olem4  22908  lognegb  22950  logcj  22967  argimgt0  22973  logdmnrp  22998  logcnlem3  23001  logrec  23127  dcubic  23153  isppw  23364  rplogsumlem2  23646  pntpbnd1  23747  axlowdimlem16  24236  nbgrassvwo2  24414  is2wlk  24543  wwlkn0  24665  wlkiswwlk1  24666  wlklniswwlkn1  24675  wlklniswwlkn2  24676  wwlksubclwwlk  24780  el2wlkonot  24845  frg2wot1  25033  grpoinveu  25200  grpoinvf  25218  diporthcom  25605  norm1exi  26144  shmodsi  26283  shmodi  26284  dfch2  26301  orthin  26340  chssoc  26390  spansncvi  26546  kbpj  26851  lnopunilem1  26905  cnlnssadj  26975  bra11  27003  strlem4  27149  strlem5  27150  hstrlem4  27157  hstrlem5  27158  dmdmd  27195  mdslle1i  27212  mdslle2i  27213  mdslmd1lem1  27220  atcvatlem  27280  atcvat4i  27292  mdsymlem3  27300  bcm1n  27576  xmulcand  27594  xreceu  27595  tpr2rico  27871  mrsubff1  28851  mvhf1  28896  funpsstri  29170  sltres  29399  nofulllem1  29437  nofulllem2  29438  btwnintr  29644  idinside  29709  btwnconn1lem13  29724  wl-equsal1i  29971  dvtanlem  30039  fneval  30145  ismtybndlem  30277  grpoeqdivid  30318  0rngo  30399  nzss  31198  expgrowth  31216  sbiota1  31295  usgra2pth  32192  bnj1125  33781  bj-sb4v  34085  bj-sbftv  34093  bj-equsal1t  34143  bj-ldiv  34414  bj-bary1lem1  34420  bj-bary1  34421  lcvexchlem4  34502  lcvexchlem5  34503  opcon3b  34661  2dim  34934  ps-1  34941  paddclN  35306  ltrnnid  35600  cdleme22b  35807  dihmeetlem13N  36786  dih1dimatlem  36796  dihlspsnat  36800