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  2469  abbi1dv  2470  nfcd  2485  nfcxfrd  2488  3netr4g  2546  necon3ai  2557  alral  2673  rspe  2676  rsp2e  2678  rgen2a  2681  ralrimi  2696  r19.27av  2753  mormo  2824  nrexrmo  2829  cgsex2g  2892  cgsex4g  2893  spc2egv  2942  spc3egv  2944  rspce  2951  ceqex  2970  mo2icl  3016  reu3  3027  reu6i  3028  sbc5  3071  rspesbca  3127  rmo2i  3133  sbnfc2  3197  ssrdv  3279  3sstr4g  3313  syl5eqss  3316  ss2abdv  3340  abssdv  3341  rabssdv  3347  ss2rabdv  3348  ssun1  3427  unssad  3441  unssbd  3442  uneqin  3507  reuss2  3536  ne0i  3557  reximdva0  3562  minel  3607  uneqdifeq  3639  disjsn2  3788  absneu  3795  rabsneu  3796  unsneqsn  3888  elunii  3897  dfnfc2  3910  uniss2  3923  unidif  3924  ssunieq  3925  intab  3957  iunss2  4012  iunxdif2  4015  riinrab  4042  snelpwi  4117  pwadjoin  4120  pw1disj  4168  eqrelkrdv  4215  setswith  4322  sniota  4370  eladdci  4400  findsd  4411  elsuci  4415  nnsucelr  4429  snfi  4432  ssfin  4471  eventfin  4518  oddtfin  4519  nnadjoinpw  4522  sfindbl  4531  sfinltfin  4536  vfinspnn  4542  1cvsfin  4543  vfinncvntnn  4549  vfinspclt  4553  vfinncsp  4555  vinf  4556  phi11lem1  4596  copsex2t  4609  phidisjnn  4616  3brtr4g  4672  relssdv  4850  eqrelrdv  4853  eqoprrdv  4855  opeldm  4911  imasn  5019  dminss  5042  funeu  5132  funco  5143  funun  5147  funprg  5150  funprgOLD  5151  fununi  5161  funcnvuni  5162  fnunsn  5191  fn0  5203  fnimadisj  5204  funssxp  5234  fssres  5239  feu  5243  fimacnvdisj  5245  f00  5250  f1co  5265  fores  5279  foconst  5281  foimacnv  5304  f1oun  5305  fun11iun  5306  fo00  5319  fv3  5342  nfunsn  5354  funfvbrb  5402  fvimacnv  5404  respreima  5411  fvelrn  5414  dff2  5420  dff3  5421  dffo4  5424  ffvresb  5432  fsn  5433  fpr  5438  funfvima3  5462  fvclss  5463  dff1o6  5476  isores1  5495  isoini2  5499  fununiq  5518  funsi  5521  fnoprabg  5586  ovg  5602  ndmovass  5619  ndmovdistr  5620  dmmptg  5685  trtxp  5782  fntxp  5805  qrpprod  5837  fnpprod  5844  f1opprod  5845  clos1conn  5880  clos1basesuc  5883  clos1nrel  5887  frds  5936  erth  5969  qsss  5987  ecelqsdm  5995  mapsspm  6022  mapsspw  6023  map0b  6025  mapsn  6027  f1oeng  6033  fundmen  6044  enpw1  6063  enmap2lem4  6067  enmap2  6069  enmap1lem4  6073  enprmaplem3  6079  ncelncs  6121  ncidg  6123  ncprc  6125  ncdisjun  6137  ncspw1eu  6160  nntccl  6171  fnce  6177  fce  6189  nclec  6196  lec0cg  6199  ltcpw1pwg  6203  sbthlem3  6206  dflec3  6222  nclenc  6223  lenc  6224  taddc  6230  nmembers1lem3  6271  spacis  6289  nchoicelem7  6296  nchoicelem9  6298  nchoicelem13  6302  nchoicelem14  6303  nchoicelem17  6306  fnfrec  6321  frecsuc  6323