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  2050  sb4  2070  sbft  2093  ax12indalem  2268  ax12inda2ALT  2269  gencl  3143  spsbc  3344  eqsbc3r  3393  ssnelpss  3890  uniintsn  4319  prex  4689  copsexg  4732  ordtri3  4914  posn  5068  optocl  5076  funimass1  5661  f1ocnvb  5829  eqfnfv2  5976  elpreima  6001  fconst5  6118  dff13  6154  f1ocnvfv  6172  f1ocnvfvb  6173  fliftfun  6198  eusvobj2  6277  sorpsscmpl  6575  ssonprc  6611  xpexr  6724  xpexcnv  6726  relcnvexb  6732  dmfex  6742  frxp  6893  mpt2xopn0yelv  6941  rntpos  6968  oawordeulem  7203  oalimcl  7209  odi  7228  omeulem2  7232  oeeulem  7250  erexb  7336  unxpdomlem2  7725  dif1enOLD  7752  dif1en  7753  enp1ilem  7754  findcard2  7760  isfinite2  7778  unfi  7787  fodomfib  7800  inf0  8038  rankxplim2  8298  scott0  8304  ficardom  8342  cardaleph  8470  dfac5  8509  cflim2  8643  fin23lem23  8706  fin23lem28  8720  isf32lem5  8737  domtriomlem  8822  ac6num  8859  zorn2lem5  8880  zorn2lem6  8881  iunfo  8914  axrepndlem2  8968  axregnd  8981  axregndOLD  8982  hargch  9051  addcanpi  9277  mulcanpi  9278  indpi  9285  ltaddnq  9352  ltexnq  9353  prlem934  9411  ltaddpr2  9413  ltaprlem  9422  supsrlem  9488  ssxr  9654  ltxrlt  9655  addcan  9763  addcan2  9764  neg11  9870  negreb  9884  mulcand  10182  receu  10194  lemul1a  10396  cju  10532  nn1suc  10557  nnaddcl  10558  nndivtr  10577  znegclb  10900  zmulcl  10911  zeo  10946  uz11  11104  uzp1  11115  eqreznegel  11167  rpnnen1  11213  xrltne  11366  xneg11  11414  xnegdi  11440  xrsupss  11500  xrinfmss  11501  elfznelfzob  11884  modadd1  12001  modmul1  12008  om2uzlti  12029  bccmpl  12355  hashen  12388  fz1eqb  12394  hashfn  12411  hashnn0n0nn  12426  hashtpg  12489  eqwrd  12547  ccatopth  12658  ccatopth2  12659  swrdccatin2  12675  swrdccat3a  12682  cj11  12958  rennim  13035  cnpart  13036  sqrmo  13048  sqrtgt0  13055  sqreulem  13155  sqreu  13156  lo1o1  13318  lo1eq  13354  rlimeq  13355  sumss  13509  cvgcmp  13593  efne0  13693  dvdseq  13892  divalglem8  13917  bitsinv1lem  13950  pcfac  14277  prmreclem3  14295  sectmon  15033  yoniso  15412  lublecllem  15475  oduposb  15623  mgmb1mgm1  15783  grpinveu  15894  mulgass  15982  galcan  16147  symg1bas  16226  cayleylem2  16243  odbezout  16386  odeq1  16388  dprddomcld  16835  dvreq1  17143  unitrrg  17741  coe1tm  18113  frgpcyg  18407  obslbs  18556  tgss3  19282  uptx  19889  txindislem  19897  qtopeu  19980  hmeocnvb  20038  qtophmeo  20081  trufil  20174  ufinffr  20193  ghmcnp  20376  tgioo  21064  lmmcvg  21463  bcth3  21533  ovolunlem1a  21670  vitali  21785  ismbf  21800  ismbfcn  21801  rolle  22154  itgsubstlem  22212  vieta1lem2  22469  elqaalem3  22479  aacjcl  22485  efif1olem4  22693  lognegb  22730  logcj  22747  argimgt0  22753  logdmnrp  22778  logcnlem3  22781  logrec  22907  dcubic  22933  isppw  23144  rplogsumlem2  23426  pntpbnd1  23527  axlowdimlem16  23964  nbgrassvwo2  24142  is2wlk  24271  wwlkn0  24393  wlkiswwlk1  24394  wlklniswwlkn1  24403  wlklniswwlkn2  24404  wwlksubclwwlk  24508  el2wlkonot  24573  frg2wot1  24762  grpoinveu  24928  grpoinvf  24946  diporthcom  25333  norm1exi  25872  shmodsi  26011  shmodi  26012  dfch2  26029  orthin  26068  chssoc  26118  spansncvi  26274  kbpj  26579  lnopunilem1  26633  cnlnssadj  26703  bra11  26731  strlem4  26877  strlem5  26878  hstrlem4  26885  hstrlem5  26886  dmdmd  26923  mdslle1i  26940  mdslle2i  26941  mdslmd1lem1  26948  atcvatlem  27008  atcvat4i  27020  mdsymlem3  27028  bcm1n  27296  xmulcand  27313  xreceu  27314  tpr2rico  27558  fprodser  28686  funpsstri  28800  sltres  29029  nofulllem1  29067  nofulllem2  29068  btwnintr  29274  idinside  29339  btwnconn1lem13  29354  wl-equsal1i  29601  dvtanlem  29669  fneval  29787  ismtybndlem  29933  grpoeqdivid  29974  0rngo  30055  nzss  30850  expgrowth  30868  sbiota1  30947  usgra2pth  31849  bnj1125  33145  bj-sb4v  33436  bj-sbftv  33444  bj-equsal1t  33494  bj-ldiv  33764  bj-bary1lem1  33770  bj-bary1  33771  lcvexchlem4  33852  lcvexchlem5  33853  opcon3b  34011  2dim  34284  ps-1  34291  paddclN  34656  ltrnnid  34950  cdleme22b  35155  dihmeetlem13N  36134  dih1dimatlem  36144  dihlspsnat  36148