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  5480  pofun  5564  epweon  7751  ord2eln012  8461  disjen  9098  php3  9173  sdom1  9189  sdom1OLD  9190  wemappo  9502  cnfcom2lem  9654  zfregs2  9686  cfsuc  10210  fin1a2lem12  10364  ac6num  10432  canth4  10600  pwfseqlem3  10613  gchpwdom  10623  gchaleph  10624  gchhar  10632  difreicc  13445  fzpreddisj  13534  ccatalpha  14558  s3iunsndisj  14934  fprodntriv  15908  fprodn0f  15957  lcmfunsnlem2lem2  16609  prmreclem5  16891  cidpropd  17671  gsumpropd2lem  18606  isnsgrp  18650  isnmnd  18665  mulgfval  19001  odinf  19493  frgpnabllem1  19803  ablfac1lem  20000  ablsimpgfindlem2  20040  frlmssuvc2  21704  psdmul  22053  lmmo  23267  xkohaus  23540  snfil  23751  supfil  23782  hauspwpwf1  23874  tsmsfbas  24015  reconnlem2  24716  minveclem3b  25328  dvply1  26191  taylthlem2  26282  taylthlem2OLD  26283  wilthlem2  26979  lgseisenlem1  27286  nosepon  27577  axlowdimlem6  28874  elntg2  28912  structiedg0val  28949  snstriedgval  28965  incistruhgr  29006  umgr2edg1  29138  umgr2edgneu  29141  wlkp1lem1  29601  eupth2eucrct  30146  4cycl2vnunb  30219  frgrncvvdeqlem1  30228  n0lplig  30412  addsqnot2reu  32415  ssmxidllem  33444  fldext2chn  33718  qqhf  33976  hgt750lemb  34647  bnj1417  35031  subfacp1lem1  35166  fmlasucdisj  35386  prv0  35417  pocnv  35750  wsuclb  35816  filnetlem4  36369  weiunfr  36455  bj-ab0  36896  topdifinffinlem  37335  relowlpssretop  37352  finxpnom  37389  heibor1lem  37803  notornotel2  38090  pmap0  39759  mapdh6eN  41734  mapdh7dN  41744  hdmap1l6e  41808  dvrelogpow2b  42056  aks4d1p1p4  42059  negn0nposznnd  42270  jm2.23  42985  rpnnen3lem  43020  fnwe2lem2  43040  oaordnrex  43284  omnord1ex  43293  oenord1ex  43304  nlimsuc  43430  nlim1NEW  43431  nlim2NEW  43432  nlim3  43433  nlim4  43434  imsqrtvalex  43635  fzdifsuc2  45308  icoiccdif  45522  climrec  45601  sumnnodd  45628  lptioo2  45629  lptioo1  45630  limcresiooub  45640  limcresioolb  45641  icccncfext  45885  cncfiooicclem1  45891  dvmptfprodlem  45942  stoweidlem34  46032  stoweidlem39  46037  stoweidlem59  46057  stirlinglem8  46079  dirkercncflem2  46102  fourierdlem12  46117  fourierdlem40  46145  fourierdlem42  46147  fourierdlem48  46152  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem78  46182  fourierdlem93  46197  fourierdlem103  46207  fourierdlem104  46208  elaa2  46232  sge0split  46407  iundjiun  46458  meaiininclem  46484  preimagelt  46697  preimalegt  46698  et-ltneverrefl  46869  otiunsndisjX  47280  fun2dmnopgexmpl  47285  0nelsetpreimafv  47391  ichnreuop  47473  gpg3kgrtriexlem5  48078  0nodd  48158  cznnring  48250  iineq0  48808