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:  otiunsndisj  4753  pofun  4816  disjen  7674  php3  7703  sdom1  7719  wemappo  7974  cnfcom2lem  8145  cnfcom2lemOLD  8153  zfregs2  8164  cfsuc  8637  fin1a2lem12  8791  ac6num  8859  canth4  9025  pwfseqlem3  9038  gchpwdom  9048  gchaleph  9049  gchhar  9057  difreicc  11652  fzpreddisj  11729  lsw0  12551  prmreclem5  14297  ramcl2lem  14386  cidpropd  14966  gsumpropd2lem  15827  odinf  16391  frgpnabllem1  16680  ablfac1lem  16921  frlmssuvc2  18621  frlmssuvc2OLD  18623  lmmo  19675  xkohaus  19917  snfil  20128  supfil  20159  hauspwpwf1  20251  tsmsfbas  20389  reconnlem2  21095  minveclem3b  21606  dvply1  22442  taylthlem2  22531  wilthlem2  23099  perfectlem2  23261  lgseisenlem1  23380  axlowdimlem6  23954  isusgra0  24051  usgraop  24054  usgra2edg1  24087  nbgra0edg  24136  cusgrares  24176  uvtx01vtx  24196  spthispth  24279  4cycl2vnunb  24721  frgrawopreglem4  24752  2spotdisj  24766  2spotiundisj  24767  qqhf  27631  signstfvneq0  28197  subfacp1lem1  28291  fprodntriv  28679  wsuclem  28986  wsuclb  28989  nofulllem5  29071  filnetlem4  29830  heibor1lem  29936  jm2.23  30570  rpnnen3lem  30605  fnwe2lem2  30629  lcmgcdlem  30840  jcn  31037  icoiccdif  31156  climrec  31173  sumnnodd  31200  lptioo2  31201  lptioo1  31202  limcresiooub  31212  limcresioolb  31213  icccncfext  31254  cncfiooicclem1  31260  stoweidlem34  31362  stoweidlem39  31367  stoweidlem59  31387  stirlinglem8  31409  dirkercncflem2  31432  fourierdlem12  31447  fourierdlem40  31475  fourierdlem42  31477  fourierdlem48  31483  fourierdlem74  31509  fourierdlem75  31510  fourierdlem76  31511  fourierdlem78  31513  fourierdlem93  31528  fourierdlem103  31538  fourierdlem104  31539  otiunsndisjX  31796  usg2edgneu  31907  bnj1417  33194  bj-abfal  33573  pmap0  34579  mapdh6eN  36555  mapdh7dN  36565  hdmap1l6e  36630