Theorem sylnibr 329

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 224	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	sylnib 328	1 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  otiunsndisj  5500  pofun  5584  epweon  7774  ord2eln012  8514  disjen  9153  php3  9228  php3OLD  9238  sdom1  9255  sdom1OLD  9256  wemappo  9568  cnfcom2lem  9720  zfregs2  9752  cfsuc  10276  fin1a2lem12  10430  ac6num  10498  canth4  10666  pwfseqlem3  10679  gchpwdom  10689  gchaleph  10690  gchhar  10698  difreicc  13506  fzpreddisj  13595  ccatalpha  14616  s3iunsndisj  14992  fprodntriv  15963  fprodn0f  16012  lcmfunsnlem2lem2  16663  prmreclem5  16945  cidpropd  17727  gsumpropd2lem  18662  isnsgrp  18706  isnmnd  18721  mulgfval  19057  odinf  19549  frgpnabllem1  19859  ablfac1lem  20056  ablsimpgfindlem2  20096  frlmssuvc2  21760  psdmul  22109  lmmo  23323  xkohaus  23596  snfil  23807  supfil  23838  hauspwpwf1  23930  tsmsfbas  24071  reconnlem2  24772  minveclem3b  25385  dvply1  26248  taylthlem2  26339  taylthlem2OLD  26340  wilthlem2  27036  lgseisenlem1  27343  nosepon  27634  axlowdimlem6  28931  elntg2  28969  structiedg0val  29006  snstriedgval  29022  incistruhgr  29063  umgr2edg1  29195  umgr2edgneu  29198  wlkp1lem1  29658  eupth2eucrct  30203  4cycl2vnunb  30276  frgrncvvdeqlem1  30285  n0lplig  30469  addsqnot2reu  32472  ssmxidllem  33493  fldext2chn  33767  qqhf  34022  hgt750lemb  34693  bnj1417  35077  subfacp1lem1  35206  fmlasucdisj  35426  prv0  35457  pocnv  35785  wsuclb  35851  filnetlem4  36404  weiunfr  36490  bj-ab0  36931  topdifinffinlem  37370  relowlpssretop  37387  finxpnom  37424  heibor1lem  37838  notornotel2  38125  pmap0  39789  mapdh6eN  41764  mapdh7dN  41774  hdmap1l6e  41838  dvrelogpow2b  42086  aks4d1p1p4  42089  negn0nposznnd  42300  jm2.23  42995  rpnnen3lem  43030  fnwe2lem2  43050  oaordnrex  43294  omnord1ex  43303  oenord1ex  43314  nlimsuc  43440  nlim1NEW  43441  nlim2NEW  43442  nlim3  43443  nlim4  43444  imsqrtvalex  43645  fzdifsuc2  45319  icoiccdif  45533  climrec  45612  sumnnodd  45639  lptioo2  45640  lptioo1  45641  limcresiooub  45651  limcresioolb  45652  icccncfext  45896  cncfiooicclem1  45902  dvmptfprodlem  45953  stoweidlem34  46043  stoweidlem39  46048  stoweidlem59  46068  stirlinglem8  46090  dirkercncflem2  46113  fourierdlem12  46128  fourierdlem40  46156  fourierdlem42  46158  fourierdlem48  46163  fourierdlem74  46189  fourierdlem75  46190  fourierdlem76  46191  fourierdlem78  46193  fourierdlem93  46208  fourierdlem103  46218  fourierdlem104  46219  elaa2  46243  sge0split  46418  iundjiun  46469  meaiininclem  46495  preimagelt  46708  preimalegt  46709  et-ltneverrefl  46880  otiunsndisjX  47288  fun2dmnopgexmpl  47293  0nelsetpreimafv  47384  ichnreuop  47466  gpg3kgrtriexlem5  48069  0nodd  48125  cznnring  48217  iineq0  48778