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  5468  pofun  5550  epweon  7722  ord2eln012  8425  disjen  9065  php3  9136  sdom1  9153  wemappo  9457  cnfcom2lem  9613  zfregs2  9645  cfsuc  10170  fin1a2lem12  10324  ac6num  10392  canth4  10561  pwfseqlem3  10574  gchpwdom  10584  gchaleph  10585  gchhar  10593  difreicc  13428  fzpreddisj  13518  ccatalpha  14547  s3iunsndisj  14921  fprodntriv  15898  fprodn0f  15947  lcmfunsnlem2lem2  16599  prmreclem5  16882  cidpropd  17667  gsumpropd2lem  18638  isnsgrp  18682  isnmnd  18697  mulgfval  19036  odinf  19529  frgpnabllem1  19839  ablfac1lem  20036  ablsimpgfindlem2  20076  frlmssuvc2  21785  psdmul  22142  lmmo  23355  xkohaus  23628  snfil  23839  supfil  23870  hauspwpwf1  23962  tsmsfbas  24103  reconnlem2  24803  minveclem3b  25405  dvply1  26260  taylthlem2  26351  taylthlem2OLD  26352  wilthlem2  27046  lgseisenlem1  27352  nosepon  27643  axlowdimlem6  29030  elntg2  29068  structiedg0val  29105  snstriedgval  29121  incistruhgr  29162  umgr2edg1  29294  umgr2edgneu  29297  wlkp1lem1  29755  eupth2eucrct  30302  4cycl2vnunb  30375  frgrncvvdeqlem1  30384  n0lplig  30569  addsqnot2reu  32570  ssmxidllem  33548  evlextv  33701  esplyindfv  33735  vietalem  33738  fldext2chn  33888  qqhf  34146  hgt750lemb  34816  bnj1417  35199  fineqvnttrclse  35284  subfacp1lem1  35377  fmlasucdisj  35597  prv0  35628  pocnv  35961  wsuclb  36024  filnetlem4  36579  weiunfr  36665  bj-ab0  37231  topdifinffinlem  37677  relowlpssretop  37694  finxpnom  37731  heibor1lem  38144  notornotel2  38431  pmap0  40225  mapdh6eN  42200  mapdh7dN  42210  hdmap1l6e  42274  dvrelogpow2b  42521  aks4d1p1p4  42524  negn0nposznnd  42728  jm2.23  43442  rpnnen3lem  43477  fnwe2lem2  43497  oaordnrex  43741  omnord1ex  43750  oenord1ex  43761  nlimsuc  43886  nlim1NEW  43887  nlim2NEW  43888  nlim3  43889  nlim4  43890  imsqrtvalex  44091  fzdifsuc2  45761  icoiccdif  45972  climrec  46051  sumnnodd  46078  lptioo2  46079  lptioo1  46080  limcresiooub  46088  limcresioolb  46089  icccncfext  46333  cncfiooicclem1  46339  dvmptfprodlem  46390  stoweidlem34  46480  stoweidlem39  46485  stoweidlem59  46505  stirlinglem8  46527  dirkercncflem2  46550  fourierdlem12  46565  fourierdlem40  46593  fourierdlem42  46595  fourierdlem48  46600  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem78  46630  fourierdlem93  46645  fourierdlem103  46655  fourierdlem104  46656  elaa2  46680  sge0split  46855  iundjiun  46906  meaiininclem  46932  preimagelt  47145  preimalegt  47146  et-ltneverrefl  47317  otiunsndisjX  47739  fun2dmnopgexmpl  47744  0nelsetpreimafv  47862  ichnreuop  47944  gpg3kgrtriexlem5  48575  0nodd  48658  cznnring  48750  iineq0  49307