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  5497  pofun  5581  fvtp0  7199  epweon  7774  ord2eln012  8484  disjen  9132  php3  9203  sdom1  9220  wemappo  9521  cnfcom2lem  9680  zfregs2  9712  cfsuc  10259  fin1a2lem12  10413  ac6num  10481  canth4  10656  pwfseqlem3  10669  gchpwdom  10679  gchaleph  10680  gchhar  10688  difreicc  13537  fzpreddisj  13628  ccatalpha  14660  s3iunsndisj  15041  fprodntriv  16029  fprodn0f  16078  lcmfunsnlem2lem2  16729  prmreclem5  17012  cidpropd  17798  gsumpropd2lem  18781  isnsgrp  18825  isnmnd  18840  mulgfval  19192  odinf  19690  frgpnabllem1  20000  ablfac1lem  20197  ablsimpgfindlem2  20237  frlmssuvc2  22008  psdmul  22394  lmmo  23605  xkohaus  23879  snfil  24090  supfil  24121  hauspwpwf1  24213  tsmsfbas  24354  reconnlem2  25054  minveclem3b  25656  dvply1  26514  rnplynfin  26539  taylthlem2  26610  wilthlem2  27305  lgseisenlem1  27611  nosepon  27901  axlowdimlem6  29404  elntg2  29442  structiedg0val  29479  snstriedgval  29495  incistruhgr  29536  umgr2edg1  29671  umgr2edgneu  29674  wlkp1lem1  30131  eupth2eucrct  30697  4cycl2vnunb  30770  frgrncvvdeqlem1  30779  n0lplig  30964  addsqnot2reu  32961  ssmxidllem  33876  evlextv  34052  esplyindfv  34086  vietalem  34089  fldext2chn  34238  qqhf  34496  hgt750lemb  35164  bnj1417  35550  fineqvnttrclse  35650  subfacp1lem1  35758  fmlasucdisj  35978  prv0  36009  pocnv  36342  wsuclb  36405  filnetlem4  37000  weiunfr  37086  bj-ab0  37651  topdifinffinlem  38101  relowlpssretop  38118  finxpnom  38155  heibor1lem  38559  notornotel2  38844  pmap0  40638  mapdh6eN  42613  mapdh7dN  42623  hdmap1l6e  42687  dvrelogpow2b  42934  aks4d1p1p4  42937  negn0nposznnd  43157  jm2.23  43837  rpnnen3lem  43872  fnwe2lem2  43892  oaordnrex  44136  omnord1ex  44145  oenord1ex  44156  nlimsuc  44281  nlim1NEW  44282  nlim2NEW  44283  nlim3  44284  nlim4  44285  imsqrtvalex  44486  fzdifsuc2  46143  icoiccdif  46354  climrec  46433  sumnnodd  46460  lptioo2  46461  lptioo1  46462  limcresiooub  46470  limcresioolb  46471  icccncfext  46715  cncfiooicclem1  46721  dvmptfprodlem  46772  stoweidlem34  46862  stoweidlem39  46867  stoweidlem59  46887  stirlinglem8  46909  dirkercncflem2  46932  fourierdlem12  46947  fourierdlem40  46975  fourierdlem42  46977  fourierdlem48  46982  fourierdlem74  47008  fourierdlem75  47009  fourierdlem76  47010  fourierdlem78  47012  fourierdlem93  47027  fourierdlem103  47037  fourierdlem104  47038  elaa2  47062  sge0split  47237  iundjiun  47288  meaiininclem  47314  preimagelt  47527  preimalegt  47528  et-ltneverrefl  47699  otiunsndisjX  48167  fun2dmnopgexmpl  48172  0nelsetpreimafv  48290  ichnreuop  48372  gpg3kgrtriexlem5  49003  0nodd  49085  cznnring  49177  smprngprmrng  49254  iineq0  49748