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  4662  pofun  4726  disjen  7675  php3  7704  sdom1  7718  wemappo  8010  cnfcom2lem  8151  zfregs2  8162  cfsuc  8631  fin1a2lem12  8785  ac6num  8853  canth4  9016  pwfseqlem3  9029  gchpwdom  9039  gchaleph  9040  gchhar  9048  difreicc  11708  fzpreddisj  11789  fprodntriv  13932  fprodn0f  13981  lcmfunsnlem2lem2  14548  prmreclem5  14800  ramcl2lemOLD  14899  cidpropd  15551  gsumpropd2lem  16452  isnsgrp  16467  isnmnd  16476  odinf  17150  frgpnabllem1  17445  ablfac1lem  17637  frlmssuvc2  19288  lmmo  20331  xkohaus  20603  snfil  20814  supfil  20845  hauspwpwf1  20937  tsmsfbas  21077  reconnlem2  21780  minveclem3b  22305  minveclem3bOLD  22317  dvply1  23172  taylthlem2  23264  wilthlem2  23929  lgseisenlem1  24212  axlowdimlem6  24912  isusgra0  25009  usgraop  25012  usgra2edg1  25045  nbgra0edg  25095  cusgrares  25135  uvtx01vtx  25155  spthispth  25238  4cycl2vnunb  25680  frgrawopreglem4  25710  2spotdisj  25724  2spotiundisj  25725  xrge0infssOLD  28284  qqhf  28735  signstfvneq0  29406  bnj1417  29795  subfacp1lem1  29847  pocnv  30348  wsuclem  30452  wsuclb  30455  nofulllem5  30537  filnetlem4  30979  bj-abfal  31415  topdifinffinlem  31651  relowlpssretop  31668  finxpnom  31694  heibor1lem  32042  notornotel2  32233  pmap0  33236  mapdh6eN  35214  mapdh7dN  35224  hdmap1l6e  35289  jm2.23  35758  rpnnen3lem  35793  fnwe2lem2  35816  jcn  37278  fzdifsuc2  37421  icoiccdif  37511  climrec  37558  sumnnodd  37587  lptioo2  37588  lptioo1  37589  limcresiooub  37600  limcresioolb  37601  icccncfext  37642  cncfiooicclem1  37648  dvmptfprodlem  37696  stoweidlem34  37772  stoweidlem39  37777  stoweidlem59  37797  stirlinglem8  37820  dirkercncflem2  37843  fourierdlem12  37858  fourierdlem40  37887  fourierdlem42  37889  fourierdlem42OLD  37890  fourierdlem48  37895  fourierdlem74  37921  fourierdlem75  37922  fourierdlem76  37923  fourierdlem78  37925  fourierdlem93  37940  fourierdlem103  37950  fourierdlem104  37951  elaa2  37976  sge0split  38096  iundjiun  38143  otiunsndisjX  38808  fun2dmnopgexmpl  38828  structiedg0val  38892  snstriedgval  38906  incistruhgr  38939  usgr2edg1  39035  usg2edgneu  39309  0nodd  39395  cznnring  39543