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  5505  pofun  5589  epweon  7776  ord2eln012  8484  disjen  9125  php3  9196  sdom1  9213  wemappo  9514  cnfcom2lem  9673  zfregs2  9705  cfsuc  10252  fin1a2lem12  10406  ac6num  10474  canth4  10643  pwfseqlem3  10656  gchpwdom  10666  gchaleph  10667  gchhar  10675  difreicc  13523  fzpreddisj  13614  ccatalpha  14646  s3iunsndisj  15025  fprodntriv  16015  fprodn0f  16064  lcmfunsnlem2lem2  16715  prmreclem5  16998  cidpropd  17784  gsumpropd2lem  18759  isnsgrp  18803  isnmnd  18818  mulgfval  19159  odinf  19657  frgpnabllem1  19967  ablfac1lem  20164  ablsimpgfindlem2  20204  frlmssuvc2  21975  psdmul  22359  lmmo  23567  xkohaus  23841  snfil  24052  supfil  24083  hauspwpwf1  24175  tsmsfbas  24316  reconnlem2  25016  minveclem3b  25618  dvply1  26476  taylthlem2  26568  wilthlem2  27264  lgseisenlem1  27570  nosepon  27860  axlowdimlem6  29328  elntg2  29366  structiedg0val  29403  snstriedgval  29419  incistruhgr  29460  umgr2edg1  29595  umgr2edgneu  29598  wlkp1lem1  30055  eupth2eucrct  30615  4cycl2vnunb  30688  frgrncvvdeqlem1  30697  n0lplig  30882  addsqnot2reu  32879  ssmxidllem  33796  evlextv  33972  esplyindfv  34006  vietalem  34009  fldext2chn  34158  qqhf  34416  hgt750lemb  35084  bnj1417  35470  fineqvnttrclse  35570  subfacp1lem1  35684  fmlasucdisj  35904  prv0  35935  pocnv  36268  wsuclb  36331  filnetlem4  36925  weiunfr  37011  bj-ab0  37576  topdifinffinlem  38026  relowlpssretop  38043  finxpnom  38080  heibor1lem  38493  notornotel2  38778  pmap0  40572  mapdh6eN  42547  mapdh7dN  42557  hdmap1l6e  42621  dvrelogpow2b  42868  aks4d1p1p4  42871  negn0nposznnd  43076  jm2.23  43756  rpnnen3lem  43791  fnwe2lem2  43811  oaordnrex  44055  omnord1ex  44064  oenord1ex  44075  nlimsuc  44200  nlim1NEW  44201  nlim2NEW  44202  nlim3  44203  nlim4  44204  imsqrtvalex  44405  fzdifsuc2  46062  icoiccdif  46273  climrec  46352  sumnnodd  46379  lptioo2  46380  lptioo1  46381  limcresiooub  46389  limcresioolb  46390  icccncfext  46634  cncfiooicclem1  46640  dvmptfprodlem  46691  stoweidlem34  46781  stoweidlem39  46786  stoweidlem59  46806  stirlinglem8  46828  dirkercncflem2  46851  fourierdlem12  46866  fourierdlem40  46894  fourierdlem42  46896  fourierdlem48  46901  fourierdlem74  46927  fourierdlem75  46928  fourierdlem76  46929  fourierdlem78  46931  fourierdlem93  46946  fourierdlem103  46956  fourierdlem104  46957  elaa2  46981  sge0split  47156  iundjiun  47207  meaiininclem  47233  preimagelt  47446  preimalegt  47447  et-ltneverrefl  47618  otiunsndisjX  48049  fun2dmnopgexmpl  48054  0nelsetpreimafv  48172  ichnreuop  48254  gpg3kgrtriexlem5  48885  0nodd  48968  cznnring  49060  smprngprmrng  49137  iineq0  49631