Theorem sylibr 203

Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
sylibr	|- (ph -> ch)

Proof of Theorem sylibr

Step	Hyp	Ref	Expression
1		sylibr.1	. 2 |- (ph -> ps)
2		sylibr.2	. . 3 |- (ch <-> ps)
3	2	biimpri 197	. 2 |- (ps -> ch)
4	1, 3	syl 15	1 |- (ph -> ch)

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

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 177

This theorem is referenced by:  pm5.74rd  239  bitri  240  3imtr4i  257  con2bid  319  sylanbrc  645  oplem1  930  3mix1  1124  3mix2  1125  3jca  1132  syl3anbrc  1136  inegd  1333  cad11  1399  had1  1402  nfxfrd  1571  19.29r  1597  nfdv  1639  19.39  1661  19.24  1662  19.34  1663  19.8wOLD  1693  19.8a  1756  nfd  1766  hbim1  1810  nfim1OLD  1812  spimehOLD  1821  nfan1  1881  ax12olem2  1928  spime  1976  sbn  2062  spsbe  2075  ax11eq  2193  ax11el  2194  mo  2226  eu2  2229  exmo  2249  2exeu  2281  2mo  2282  2eu6  2289  bm1.1  2338  eqrdv  2351  3eltr4g  2436  abbi2dv  2468  abbi1dv  2469  nfcd  2484  nfcxfrd  2487  3netr4g  2545  necon3ai  2556  alral  2672  rspe  2675  rsp2e  2677  rgen2a  2680  ralrimi  2695  r19.27av  2752  mormo  2823  nrexrmo  2828  cgsex2g  2891  cgsex4g  2892  spc2egv  2941  spc3egv  2943  rspce  2950  ceqex  2969  mo2icl  3015  reu3  3026  reu6i  3027  sbc5  3070  rspesbca  3126  rmo2i  3132  sbnfc2  3196  ssrdv  3278  3sstr4g  3312  syl5eqss  3315  ss2abdv  3339  abssdv  3340  rabssdv  3346  ss2rabdv  3347  ssun1  3426  unssad  3440  unssbd  3441  uneqin  3506  reuss2  3535  ne0i  3556  reximdva0  3561  minel  3606  uneqdifeq  3638  disjsn2  3787  absneu  3794  rabsneu  3795  unsneqsn  3887  elunii  3896  dfnfc2  3909  uniss2  3922  unidif  3923  ssunieq  3924  intab  3956  iunss2  4011  iunxdif2  4014  riinrab  4041  snelpwi  4116  pwadjoin  4119  pw1disj  4167  eqrelkrdv  4214  setswith  4321  sniota  4369  eladdci  4399  findsd  4410  elsuci  4414  nnsucelr  4428  snfi  4431  ssfin  4470  eventfin  4517  oddtfin  4518  nnadjoinpw  4521  sfindbl  4530  sfinltfin  4535  vfinspnn  4541  1cvsfin  4542  vfinncvntnn  4548  vfinspclt  4552  vfinncsp  4554  vinf  4555  phi11lem1  4595  copsex2t  4608  phidisjnn  4615  3brtr4g  4671  relssdv  4849  eqrelrdv  4852  eqoprrdv  4854  opeldm  4910  imasn  5018  dminss  5041  funeu  5131  funco  5142  funun  5146  funprg  5149  funprgOLD  5150  fununi  5160  funcnvuni  5161  fnunsn  5190  fn0  5202  fnimadisj  5203  funssxp  5233  fssres  5238  feu  5242  fimacnvdisj  5244  f00  5249  f1co  5264  fores  5278  foconst  5280  foimacnv  5303  f1oun  5304  fun11iun  5305  fo00  5318  fv3  5341  nfunsn  5353  funfvbrb  5401  fvimacnv  5403  respreima  5410  fvelrn  5413  dff2  5419  dff3  5420  dffo4  5423  ffvresb  5431  fsn  5432  fpr  5437  funfvima3  5461  fvclss  5462  dff1o6  5475  isores1  5494  isoini2  5498  fununiq  5517  funsi  5520  fnoprabg  5585  ovg  5601  ndmovass  5618  ndmovdistr  5619  dmmptg  5684  trtxp  5781  fntxp  5804  qrpprod  5836  fnpprod  5843  f1opprod  5844  clos1conn  5879  clos1basesuc  5882  clos1nrel  5886  frds  5935  erth  5968  qsss  5986  ecelqsdm  5994  mapsspm  6021  mapsspw  6022  map0b  6024  mapsn  6026  f1oeng  6032  fundmen  6043  enpw1  6062  enmap2lem4  6066  enmap2  6068  enmap1lem4  6072  enprmaplem3  6078  ncelncs  6120  ncidg  6122  ncprc  6124  ncdisjun  6136  ncspw1eu  6159  nntccl  6170  fnce  6176  fce  6188  nclec  6195  lec0cg  6198  ltcpw1pwg  6202  sbthlem3  6205  dflec3  6221  nclenc  6222  lenc  6223  taddc  6229  nmembers1lem3  6270  spacis  6288  nchoicelem7  6295  nchoicelem9  6297  nchoicelem13  6301  nchoicelem14  6302  nchoicelem17  6305  fnfrec  6320  frecsuc  6322