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  4644  disjen  7456  php3  7485  sdom1  7500  wemappo  7751  cnfcom2lem  7922  cnfcom2lemOLD  7930  zfregs2  7941  cfsuc  8414  fin1a2lem12  8568  ac6num  8636  canth4  8801  pwfseqlem3  8814  gchpwdom  8824  gchaleph  8825  gchhar  8833  difreicc  11403  lsw0  12250  prmreclem5  13963  ramcl2lem  14052  cidpropd  14631  odinf  16043  frgpnabllem1  16330  ablfac1lem  16542  frlmssuvc2  18061  frlmssuvc2OLD  18063  lmmo  18825  xkohaus  19067  snfil  19278  supfil  19309  hauspwpwf1  19401  tsmsfbas  19539  reconnlem2  20245  minveclem3b  20756  dvply1  21634  taylthlem2  21723  wilthlem2  22291  perfectlem2  22453  lgseisenlem1  22572  axlowdimlem6  23015  isusgra0  23097  usgra2edg1  23124  nbgra0edg  23165  cusgrares  23202  uvtx01vtx  23222  spthispth  23294  gsumpropd2lem  26092  qqhf  26268  signstfvneq0  26820  subfacp1lem1  26914  fprodntriv  27301  wsuclem  27608  wsuclb  27611  nofulllem5  27693  filnetlem4  28443  heibor1lem  28549  jm2.23  29187  rpnnen3lem  29222  fnwe2lem2  29246  climrec  29619  stoweidlem34  29672  stoweidlem39  29677  stoweidlem59  29697  stirlinglem8  29719  otiunsndisj  29975  otiunsndisjX  29976  4cycl2vnunb  30452  frgrawopreglem4  30483  2spotdisj  30497  2spotiundisj  30498  bnj1417  31731  bj-abfal  32000  pmap0  32979  mapdh6eN  34955  mapdh7dN  34965  hdmap1l6e  35030