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  5492  pofun  5576  fvtp0  7208  epweon  7791  fnwe2lem3  8151  ord2eln012  8510  disjen  9158  php3  9229  sdom1  9246  wemappo  9548  cnfcom2lem  9707  zfregs2  9739  cfsuc  10340  fin1a2lem12  10494  ac6num  10562  canth4  10737  pwfseqlem3  10750  gchpwdom  10760  gchaleph  10761  gchhar  10769  difreicc  13620  fzpreddisj  13712  ccatalpha  14745  s3iunsndisj  15128  fprodntriv  16116  fprodn0f  16165  lcmfunsnlem2lem2  16821  prmreclem5  17105  cidpropd  17891  gsumpropd2lem  18875  isnsgrp  18919  isnmnd  18934  mulgfval  19286  odinf  19784  frgpnabllem1  20094  ablfac1lem  20291  ablsimpgfindlem2  20331  frlmssuvc2  22108  psdmul  22494  lmmo  23705  xkohaus  23979  snfil  24190  supfil  24221  hauspwpwf1  24313  tsmsfbas  24454  reconnlem2  25154  minveclem3b  25756  dvply1  26612  rnplynfin  26637  taylthlem2  26708  wilthlem2  27403  lgseisenlem1  27709  nosepon  28029  axlowdimlem6  29532  elntg2  29570  structiedg0val  29607  snstriedgval  29623  incistruhgr  29664  umgr2edg1  29799  umgr2edgneu  29802  wlkp1lem1  30259  eupth2eucrct  30825  4cycl2vnunb  30898  frgrncvvdeqlem1  30907  n0lplig  31092  addsqnot2reu  33131  ssmxidllem  34046  evlextv  34222  esplyindfv  34256  vietalem  34259  fldext2chn  34408  qqhf  34666  hgt750lemb  35333  bnj1417  35719  fineqvnttrclse  35850  maxssj0  35947  subfacp1lem1  36032  fmlasucdisj  36252  prv0  36283  pocnv  36622  wsuclb  36684  filnetlem4  37263  weiunfr  37349  bj-ab0  37914  topdifinffinlem  38377  relowlpssretop  38394  finxpnom  38431  heibor1lem  38850  notornotel2  39135  pmap0  40929  mapdh6eN  42904  mapdh7dN  42914  hdmap1l6e  42978  dvrelogpow2b  43225  aks4d1p1p4  43228  negn0nposznnd  43446  jm2.23  44110  rpnnen3lem  44145  oaordnrex  44404  omnord1ex  44413  oenord1ex  44424  nlimsuc  44549  nlim1NEW  44550  nlim2NEW  44551  nlim3  44552  nlim4  44553  imsqrtvalex  44753  fzdifsuc2  46433  icoiccdif  46643  climrec  46722  sumnnodd  46749  lptioo2  46750  lptioo1  46751  limcresiooub  46759  limcresioolb  46760  icccncfext  47004  cncfiooicclem1  47010  dvmptfprodlem  47061  stoweidlem34  47151  stoweidlem39  47156  stoweidlem59  47176  stirlinglem8  47198  dirkercncflem2  47221  fourierdlem12  47236  fourierdlem40  47264  fourierdlem42  47266  fourierdlem48  47271  fourierdlem74  47297  fourierdlem75  47298  fourierdlem76  47299  fourierdlem78  47301  fourierdlem93  47316  fourierdlem103  47326  fourierdlem104  47327  elaa2  47351  sge0split  47526  iundjiun  47577  meaiininclem  47603  preimagelt  47816  preimalegt  47817  et-ltneverrefl  47988  otiunsndisjX  48456  fun2dmnopgexmpl  48461  0nelsetpreimafv  48579  ichnreuop  48661  gpg3kgrtriexlem5  49292  0nodd  49374  cznnring  49466  smprngprmrng  49543  iineq0  50038