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  5455  pofun  5537  epweon  7703  ord2eln012  8407  disjen  9042  php3  9113  sdom1  9129  wemappo  9430  cnfcom2lem  9586  zfregs2  9618  cfsuc  10143  fin1a2lem12  10297  ac6num  10365  canth4  10533  pwfseqlem3  10546  gchpwdom  10556  gchaleph  10557  gchhar  10565  difreicc  13379  fzpreddisj  13468  ccatalpha  14496  s3iunsndisj  14870  fprodntriv  15844  fprodn0f  15893  lcmfunsnlem2lem2  16545  prmreclem5  16827  cidpropd  17611  gsumpropd2lem  18582  isnsgrp  18626  isnmnd  18641  mulgfval  18977  odinf  19470  frgpnabllem1  19780  ablfac1lem  19977  ablsimpgfindlem2  20017  frlmssuvc2  21727  psdmul  22076  lmmo  23290  xkohaus  23563  snfil  23774  supfil  23805  hauspwpwf1  23897  tsmsfbas  24038  reconnlem2  24738  minveclem3b  25350  dvply1  26213  taylthlem2  26304  taylthlem2OLD  26305  wilthlem2  27001  lgseisenlem1  27308  nosepon  27599  axlowdimlem6  28920  elntg2  28958  structiedg0val  28995  snstriedgval  29011  incistruhgr  29052  umgr2edg1  29184  umgr2edgneu  29187  wlkp1lem1  29645  eupth2eucrct  30189  4cycl2vnunb  30262  frgrncvvdeqlem1  30271  n0lplig  30455  addsqnot2reu  32457  ssmxidllem  33430  fldext2chn  33733  qqhf  33991  hgt750lemb  34661  bnj1417  35045  fineqvnttrclse  35136  subfacp1lem1  35215  fmlasucdisj  35435  prv0  35466  pocnv  35799  wsuclb  35862  filnetlem4  36415  weiunfr  36501  bj-ab0  36942  topdifinffinlem  37381  relowlpssretop  37398  finxpnom  37435  heibor1lem  37849  notornotel2  38136  pmap0  39804  mapdh6eN  41779  mapdh7dN  41789  hdmap1l6e  41853  dvrelogpow2b  42101  aks4d1p1p4  42104  negn0nposznnd  42315  jm2.23  43029  rpnnen3lem  43064  fnwe2lem2  43084  oaordnrex  43328  omnord1ex  43337  oenord1ex  43348  nlimsuc  43474  nlim1NEW  43475  nlim2NEW  43476  nlim3  43477  nlim4  43478  imsqrtvalex  43679  fzdifsuc2  45351  icoiccdif  45564  climrec  45643  sumnnodd  45670  lptioo2  45671  lptioo1  45672  limcresiooub  45680  limcresioolb  45681  icccncfext  45925  cncfiooicclem1  45931  dvmptfprodlem  45982  stoweidlem34  46072  stoweidlem39  46077  stoweidlem59  46097  stirlinglem8  46119  dirkercncflem2  46142  fourierdlem12  46157  fourierdlem40  46185  fourierdlem42  46187  fourierdlem48  46192  fourierdlem74  46218  fourierdlem75  46219  fourierdlem76  46220  fourierdlem78  46222  fourierdlem93  46237  fourierdlem103  46247  fourierdlem104  46248  elaa2  46272  sge0split  46447  iundjiun  46498  meaiininclem  46524  preimagelt  46737  preimalegt  46738  et-ltneverrefl  46909  otiunsndisjX  47310  fun2dmnopgexmpl  47315  0nelsetpreimafv  47421  ichnreuop  47503  gpg3kgrtriexlem5  48118  0nodd  48201  cznnring  48293  iineq0  48851