Theorem sylnibr 297

Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)

Hypotheses

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

Assertion

Ref	Expression
sylnibr	|- ( ph -> -. ch )

Proof of Theorem sylnibr

Step	Hyp	Ref	Expression
1		sylnibr.1	. 2 |- ( ph -> -. ps )
2		sylnibr.2	. . 3 |- ( ch <-> ps )
3	2	bicomi 194	. 2 |- ( ps <-> ch )
4	1, 3	sylnib 296	1 |- ( ph -> -. ch )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177

This theorem is referenced by:  pofun  4479  disjen  7223  php3  7252  sdom1  7267  wemappo  7474  cnfcom2lem  7614  zfregs2  7625  cfsuc  8093  fin1a2lem12  8247  ac6num  8315  canth4  8478  pwfseqlem3  8491  gchhar  8502  gchpwdom  8505  gchaleph  8506  difreicc  10984  prmreclem5  13243  ramcl2lem  13332  cidpropd  13891  odinf  15154  frgpnabllem1  15439  ablfac1lem  15581  lmmo  17398  xkohaus  17638  snfil  17849  supfil  17880  hauspwpwf1  17972  tsmsfbas  18110  reconnlem2  18811  minveclem3b  19282  dvply1  20154  taylthlem2  20243  wilthlem2  20805  perfectlem2  20967  lgseisenlem1  21086  isusgra0  21329  usgra2edg1  21356  nbgra0edg  21397  cusgrares  21434  uvtx01vtx  21454  spthispth  21526  gsumpropd2lem  24173  qqhf  24323  subfacp1lem1  24818  fprodntriv  25221  nofulllem5  25574  axlowdimlem6  25790  filnetlem4  26300  heibor1lem  26408  jm2.23  26957  rpnnen3lem  26992  fnwe2lem2  27016  frlmssuvc2  27115  climrec  27596  stoweidlem34  27650  stoweidlem39  27655  stoweidlem59  27675  stirlinglem8  27697  otiunsndisj  27954  otiunsndisjX  27955  swrd0  28002  frgra2v  28103  4cycl2vnunb  28121  frgrawopreglem4  28150  2spotdisj  28164  2spotiundisj  28165  bnj1417  29116  pmap0  30247  mapdh6eN  32223  mapdh7dN  32233  hdmap1l6e  32298

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 178