Theorem sylnibr 305

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 202	. 2 |- ( ps <-> ch )
4	1, 3	sylnib 304	1 |- ( ph -> -. ch )

Syntax hints:   -. wn 3   -> 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:  pofun  4760  disjen  7573  php3  7602  sdom1  7618  wemappo  7869  cnfcom2lem  8040  cnfcom2lemOLD  8048  zfregs2  8059  cfsuc  8532  fin1a2lem12  8686  ac6num  8754  canth4  8920  pwfseqlem3  8933  gchpwdom  8943  gchaleph  8944  gchhar  8952  difreicc  11529  fzpreddisj  11616  lsw0  12380  prmreclem5  14094  ramcl2lem  14183  cidpropd  14763  gsumpropd2lem  15619  odinf  16180  frgpnabllem1  16467  ablfac1lem  16686  frlmssuvc2  18340  frlmssuvc2OLD  18342  lmmo  19111  xkohaus  19353  snfil  19564  supfil  19595  hauspwpwf1  19687  tsmsfbas  19825  reconnlem2  20531  minveclem3b  21042  dvply1  21878  taylthlem2  21967  wilthlem2  22535  perfectlem2  22697  lgseisenlem1  22816  axlowdimlem6  23340  isusgra0  23422  usgra2edg1  23449  nbgra0edg  23490  cusgrares  23527  uvtx01vtx  23547  spthispth  23619  qqhf  26555  signstfvneq0  27112  subfacp1lem1  27206  fprodntriv  27594  wsuclem  27901  wsuclb  27904  nofulllem5  27986  filnetlem4  28745  heibor1lem  28851  jm2.23  29488  rpnnen3lem  29523  fnwe2lem2  29547  climrec  29919  stoweidlem34  29972  stoweidlem39  29977  stoweidlem59  29997  stirlinglem8  30019  otiunsndisj  30275  otiunsndisjX  30276  4cycl2vnunb  30752  frgrawopreglem4  30783  2spotdisj  30797  2spotiundisj  30798  bnj1417  32345  bj-abfal  32722  pmap0  33728  mapdh6eN  35704  mapdh7dN  35714  hdmap1l6e  35779