Theorem sylnibr 306

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

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

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 188

This theorem is referenced by:  otiunsndisj  4727  pofun  4791  disjen  7735  php3  7764  sdom1  7778  wemappo  8064  cnfcom2lem  8205  zfregs2  8216  cfsuc  8685  fin1a2lem12  8839  ac6num  8907  canth4  9071  pwfseqlem3  9084  gchpwdom  9094  gchaleph  9095  gchhar  9103  difreicc  11762  fzpreddisj  11843  fprodntriv  13974  fprodn0f  14023  lcmfunsnlem2lem2  14583  prmreclem5  14827  ramcl2lemOLD  14926  cidpropd  15566  gsumpropd2lem  16467  isnsgrp  16482  isnmnd  16491  odinf  17152  frgpnabllem1  17444  ablfac1lem  17636  frlmssuvc2  19284  lmmo  20327  xkohaus  20599  snfil  20810  supfil  20841  hauspwpwf1  20933  tsmsfbas  21073  reconnlem2  21756  minveclem3b  22263  dvply1  23105  taylthlem2  23194  wilthlem2  23859  lgseisenlem1  24140  axlowdimlem6  24823  isusgra0  24920  usgraop  24923  usgra2edg1  24956  nbgra0edg  25005  cusgrares  25045  uvtx01vtx  25065  spthispth  25148  4cycl2vnunb  25590  frgrawopreglem4  25620  2spotdisj  25634  2spotiundisj  25635  xrge0infss  28181  qqhf  28629  signstfvneq0  29249  bnj1417  29638  subfacp1lem1  29690  pocnv  30191  wsuclem  30295  wsuclb  30298  nofulllem5  30380  filnetlem4  30822  bj-abfal  31259  topdifinffinlem  31484  relowlpssretop  31501  heibor1lem  31845  notornotel2  32036  pmap0  33039  mapdh6eN  35017  mapdh7dN  35027  hdmap1l6e  35092  jm2.23  35557  rpnnen3lem  35592  fnwe2lem2  35615  jcn  37008  fzdifsuc2  37139  icoiccdif  37210  climrec  37253  sumnnodd  37282  lptioo2  37283  lptioo1  37284  limcresiooub  37295  limcresioolb  37296  icccncfext  37337  cncfiooicclem1  37343  dvmptfprodlem  37388  stoweidlem34  37464  stoweidlem39  37469  stoweidlem59  37489  stirlinglem8  37512  dirkercncflem2  37535  fourierdlem12  37550  fourierdlem40  37578  fourierdlem42  37580  fourierdlem48  37586  fourierdlem74  37612  fourierdlem75  37613  fourierdlem76  37614  fourierdlem78  37616  fourierdlem93  37631  fourierdlem103  37641  fourierdlem104  37642  elaa2  37666  etransc  37715  sge0split  37785  iundjiun  37807  otiunsndisjX  38378  usg2edgneu  38482  0nodd  38568  cznnring  38716