Theorem xchnxbir 333

Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)

Hypotheses

Ref	Expression
xchnxbir.1	⊢ (¬ 𝜑 ↔ 𝜓)
xchnxbir.2	⊢ (𝜒 ↔ 𝜑)

Assertion

Ref	Expression
xchnxbir	⊢ (¬ 𝜒 ↔ 𝜓)

Proof of Theorem xchnxbir

Step	Hyp	Ref	Expression
1		xchnxbir.1	. 2 ⊢ (¬ 𝜑 ↔ 𝜓)
2		xchnxbir.2	. . 3 ⊢ (𝜒 ↔ 𝜑)
3	2	bicomi 224	. 2 ⊢ (𝜑 ↔ 𝜒)
4	1, 3	xchnxbi 332	1 ⊢ (¬ 𝜒 ↔ 𝜓)

Syntax hints:  ¬ wn 3   ↔ 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:  3ioran  1105  3ianor  1106  hadnot  1598  cadnot  1611  2exanali  1857  nabbib  3042  nelb  3231  nsspssun  4273  undif3  4305  2nreu  4449  intirr  6140  ordtri3or  6417  nf1const  7323  nf1oconst  7324  frxp  8149  ressuppssdif  8208  suppofssd  8226  naddcllem  8712  domunfican  9358  ssfin4  10347  prinfzo0  13734  swrdnnn0nd  14690  swrdnd0  14691  lcmfunsnlem2lem1  16671  ncoprmlnprm  16761  prm23ge5  16848  smndex2dnrinv  18940  symgfix2  19448  gsumdixp  20332  cnfldfun  21395  cnfldfunOLD  21408  symgmatr01lem  22674  ppttop  23029  zclmncvs  25195  mdegleb  26117  2lgslem3  27462  trlsegvdeg  30255  strlem1  32278  difrab2  32525  isarchi  33171  bnj1189  35001  dfacycgr1  35128  fmlasucdisj  35383  dfon3  35873  wl-3xornot  37463  poimirlem18  37624  poimirlem21  37627  poimirlem30  37636  poimirlem31  37637  ftc1anclem3  37681  hdmaplem4  41756  mapdh9a  41771  onsupmaxb  43227  dflim5  43318  faosnf0.11b  43416  ifpnot23  43467  ifpdfxor  43476  ifpnim1  43486  ifpnim2  43488  dfsucon  43512  ntrneineine1lem  44073  disjrnmpt2  45130  aiotavb  47039  dfatprc  47079  ndmafv2nrn  47171  nfunsnafv2  47174  oddneven  47568  usgrexmpl2trifr  47931