Theorem sylnibr 332

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	⊢ (𝜑 → ¬ 𝜓)
sylnibr.2	⊢ (𝜒 ↔ 𝜓)

Assertion

Ref	Expression
sylnibr	⊢ (𝜑 → ¬ 𝜒)

Proof of Theorem sylnibr

Step	Hyp	Ref	Expression
1		sylnibr.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		sylnibr.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	2	bicomi 227	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	sylnib 331	1 ⊢ (𝜑 → ¬ 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  otiunsndisj  5493  pofun  5577  fvtp0  7204  epweon  7787  ord2eln012  8498  disjen  9146  php3  9217  sdom1  9234  wemappo  9536  cnfcom2lem  9695  zfregs2  9727  cfsuc  10328  fin1a2lem12  10482  ac6num  10550  canth4  10725  pwfseqlem3  10738  gchpwdom  10748  gchaleph  10749  gchhar  10757  difreicc  13608  fzpreddisj  13700  ccatalpha  14733  s3iunsndisj  15114  fprodntriv  16102  fprodn0f  16151  lcmfunsnlem2lem2  16807  prmreclem5  17091  cidpropd  17877  gsumpropd2lem  18861  isnsgrp  18905  isnmnd  18920  mulgfval  19272  odinf  19770  frgpnabllem1  20080  ablfac1lem  20277  ablsimpgfindlem2  20317  frlmssuvc2  22094  psdmul  22480  lmmo  23691  xkohaus  23965  snfil  24176  supfil  24207  hauspwpwf1  24299  tsmsfbas  24440  reconnlem2  25140  minveclem3b  25742  dvply1  26598  rnplynfin  26623  taylthlem2  26694  wilthlem2  27389  lgseisenlem1  27695  nosepon  28015  axlowdimlem6  29518  elntg2  29556  structiedg0val  29593  snstriedgval  29609  incistruhgr  29650  umgr2edg1  29785  umgr2edgneu  29788  wlkp1lem1  30245  eupth2eucrct  30811  4cycl2vnunb  30884  frgrncvvdeqlem1  30893  n0lplig  31078  addsqnot2reu  33075  ssmxidllem  33991  evlextv  34167  esplyindfv  34201  vietalem  34204  fldext2chn  34353  qqhf  34611  hgt750lemb  35278  bnj1417  35664  fineqvnttrclse  35775  subfacp1lem1  35923  fmlasucdisj  36143  prv0  36174  pocnv  36507  wsuclb  36570  filnetlem4  37149  weiunfr  37235  bj-ab0  37800  topdifinffinlem  38250  relowlpssretop  38267  finxpnom  38304  heibor1lem  38723  notornotel2  39008  pmap0  40802  mapdh6eN  42777  mapdh7dN  42787  hdmap1l6e  42851  dvrelogpow2b  43098  aks4d1p1p4  43101  negn0nposznnd  43319  jm2.23  43982  rpnnen3lem  44017  fnwe2lem2  44037  oaordnrex  44281  omnord1ex  44290  oenord1ex  44301  nlimsuc  44426  nlim1NEW  44427  nlim2NEW  44428  nlim3  44429  nlim4  44430  imsqrtvalex  44631  fzdifsuc2  46295  icoiccdif  46505  climrec  46584  sumnnodd  46611  lptioo2  46612  lptioo1  46613  limcresiooub  46621  limcresioolb  46622  icccncfext  46866  cncfiooicclem1  46872  dvmptfprodlem  46923  stoweidlem34  47013  stoweidlem39  47018  stoweidlem59  47038  stirlinglem8  47060  dirkercncflem2  47083  fourierdlem12  47098  fourierdlem40  47126  fourierdlem42  47128  fourierdlem48  47133  fourierdlem74  47159  fourierdlem75  47160  fourierdlem76  47161  fourierdlem78  47163  fourierdlem93  47178  fourierdlem103  47188  fourierdlem104  47189  elaa2  47213  sge0split  47388  iundjiun  47439  meaiininclem  47465  preimagelt  47678  preimalegt  47679  et-ltneverrefl  47850  otiunsndisjX  48318  fun2dmnopgexmpl  48323  0nelsetpreimafv  48441  ichnreuop  48523  gpg3kgrtriexlem5  49154  0nodd  49236  cznnring  49328  smprngprmrng  49405  iineq0  49899