Theorem sylnibr 311

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

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

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 190

This theorem is referenced by:  otiunsndisj  4720  pofun  4789  disjen  7754  php3  7783  sdom1  7797  wemappo  8089  cnfcom2lem  8231  zfregs2  8242  cfsuc  8712  fin1a2lem12  8866  ac6num  8934  canth4  9097  pwfseqlem3  9110  gchpwdom  9120  gchaleph  9121  gchhar  9129  difreicc  11792  fzpreddisj  11873  fprodntriv  14044  fprodn0f  14093  lcmfunsnlem2lem2  14660  prmreclem5  14912  ramcl2lemOLD  15011  cidpropd  15663  gsumpropd2lem  16564  isnsgrp  16579  isnmnd  16588  odinf  17262  frgpnabllem1  17557  ablfac1lem  17749  frlmssuvc2  19401  lmmo  20444  xkohaus  20716  snfil  20927  supfil  20958  hauspwpwf1  21050  tsmsfbas  21190  reconnlem2  21893  minveclem3b  22418  minveclem3bOLD  22430  dvply1  23285  taylthlem2  23377  wilthlem2  24042  lgseisenlem1  24325  axlowdimlem6  25025  isusgra0  25122  usgraop  25125  usgra2edg1  25158  nbgra0edg  25208  cusgrares  25248  uvtx01vtx  25268  spthispth  25351  4cycl2vnunb  25793  frgrawopreglem4  25823  2spotdisj  25837  2spotiundisj  25838  xrge0infssOLD  28389  qqhf  28838  signstfvneq0  29509  bnj1417  29898  subfacp1lem1  29950  pocnv  30452  wsuclem  30556  wsuclb  30559  nosepon  30604  nofulllem5  30643  filnetlem4  31085  bj-abfal  31553  topdifinffinlem  31794  relowlpssretop  31811  finxpnom  31837  heibor1lem  32185  notornotel2  32376  pmap0  33374  mapdh6eN  35352  mapdh7dN  35362  hdmap1l6e  35427  jm2.23  35895  rpnnen3lem  35930  fnwe2lem2  35953  jcn  37407  fzdifsuc2  37567  icoiccdif  37662  climrec  37718  sumnnodd  37747  lptioo2  37748  lptioo1  37749  limcresiooub  37760  limcresioolb  37761  icccncfext  37802  cncfiooicclem1  37808  dvmptfprodlem  37856  stoweidlem34  37932  stoweidlem39  37937  stoweidlem59  37957  stirlinglem8  37980  dirkercncflem2  38003  fourierdlem12  38018  fourierdlem40  38047  fourierdlem42  38049  fourierdlem42OLD  38050  fourierdlem48  38055  fourierdlem74  38081  fourierdlem75  38082  fourierdlem76  38083  fourierdlem78  38085  fourierdlem93  38100  fourierdlem103  38110  fourierdlem104  38111  elaa2  38136  sge0split  38288  iundjiun  38335  otiunsndisjX  39045  fun2dmnopgexmpl  39069  structiedg0val  39169  snstriedgval  39183  incistruhgr  39217  usgr2edg1  39341  usg2edgneu  39996  0nodd  40082  cznnring  40230