Theorem sylib 188

Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
sylib.1	|- (ph -> ps)
sylib.2	|- (ps <-> ch)

Assertion

Ref	Expression
sylib	|- (ph -> ch)

Proof of Theorem sylib

Step	Hyp	Ref	Expression
1		sylib.1	. 2 |- (ph -> ps)
2		sylib.2	. . 3 |- (ps <-> ch)
3	2	biimpi 186	. 2 |- (ps -> ch)
4	1, 3	syl 15	1 |- (ph -> ch)

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  bicomd  192  pm5.74d  238  bitri  240  3imtr3i  256  ord  366  orcomd  377  ancomd  438  pm4.71d  615  pm4.71rd  616  pm5.32d  620  imdistand  673  pclem6  896  3mix3  1126  ecase23d  1285  nic-ax  1438  nexdh  1589  exlimivOLD  1698  exlimd  1806  cbv3hv  1850  excomimOLD  1858  sbequi  2059  sbn  2062  spsbe  2075  spsbbi  2077  sb6rf  2091  sb9i  2094  eu2  2229  2euex  2276  2eu1  2284  eqcomd  2358  3eltr3g  2435  abbid  2466  neneqd  2532  syl5eqner  2541  3netr3g  2544  necon1bi  2559  necon4ai  2575  necon4i  2576  necomd  2599  r19.21bi  2712  nrexdv  2717  rexlimd  2735  rabbidva  2850  elisset  2869  euind  3023  rmoan  3034  reuind  3039  spsbc  3058  spesbc  3127  3sstr3g  3311  syl6sseq  3317  un00  3586  disjpss  3601  pssnel  3615  difprsn1  3847  diftpsn3  3849  difsnid  3854  ssunsn2  3865  sneqr  3872  unsneqsn  3887  intab  3956  uniintsn  3963  iinrab2  4029  riinn0  4040  rintn0  4056  preqr1  4124  preq12b  4127  iotanul  4354  iotacl  4362  dfiota4  4372  0nelsuc  4400  nnsucelrlem3  4426  nnsucelrlem4  4427  nndisjeq  4429  prepeano4  4451  ltfinirr  4457  lenltfin  4469  ssfin  4470  vfinnc  4471  ncfinlower  4483  nnpw1ex  4484  tfinltfin  4501  evenodddisj  4516  nnadjoin  4520  tfinnn  4534  sfinltfin  4535  sfin111  4536  vfinncvntsp  4549  vfinspsslem1  4550  vfinspeqtncv  4553  nulnnn  4556  phialllem1  4616  opeqex  4621  3brtr3g  4670  opeliunxp2  4822  rexxpf  4828  brel  4830  dmxp  4923  resopab2  5001  ndmima  5025  dmsnopss  5067  funeu  5131  funeu2  5132  funcnvuni  5161  imadif  5171  fneu2  5188  f00  5249  foconst  5280  foimacnv  5303  resdif  5306  resin  5307  f1ococnv2  5309  fv3  5341  dff3  5420  fsn  5432  fnressn  5438  isores1  5494  swapf1o  5511  resoprab2  5582  funoprabg  5583  fnmpt  5689  fmpt  5692  fmptd  5694  fnmpt2  5732  trtxp  5781  oqelins4  5794  qrpprod  5836  frds  5935  erth  5968  erdisj  5972  elqsn0  5993  mapsn  6026  fundmen  6043  enadjlem1  6059  enadj  6060  enpw1  6062  enprmaplem5  6080  nenpw1pwlem2  6085  mucnc  6131  ncdisjun  6136  peano4nc  6150  ncssfin  6151  ncspw1eu  6159  nntccl  6170  fnce  6176  ce0nnuli  6178  ce0addcnnul  6179  sbthlem1  6203  sbth  6206  dflec3  6221  0lt1c  6258  nmembers1lem2  6269  nncdiv3  6277  spacssnc  6284  nchoicelem12  6300  nchoicelem14  6302  nchoicelem17  6305  frecxp  6314