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  1602  cadnot  1615  2exanali  1860  nabbib  3028  nelb  3213  nsspssun  4231  undif3  4263  2nreu  4407  intirr  6091  ordtri3or  6364  nf1const  7279  nf1oconst  7280  frxp  8105  ressuppssdif  8164  suppofssd  8182  naddcllem  8640  domunfican  9272  ssfin4  10263  prinfzo0  13659  swrdnnn0nd  14621  swrdnd0  14622  lcmfunsnlem2lem1  16608  ncoprmlnprm  16698  prm23ge5  16786  smndex2dnrinv  18842  symgfix2  19346  gsumdixp  20228  cnfldfun  21278  cnfldfunOLD  21291  symgmatr01lem  22540  ppttop  22894  zclmncvs  25048  mdegleb  25969  2lgslem3  27315  trlsegvdeg  30156  strlem1  32179  difrab2  32427  isarchi  33136  bnj1189  34999  dfacycgr1  35131  fmlasucdisj  35386  dfon3  35880  wl-3xornot  37469  poimirlem18  37632  poimirlem21  37635  poimirlem30  37644  poimirlem31  37645  ftc1anclem3  37689  hdmaplem4  41768  mapdh9a  41783  onsupmaxb  43228  dflim5  43318  faosnf0.11b  43416  ifpnot23  43467  ifpdfxor  43476  ifpnim1  43486  ifpnim2  43488  dfsucon  43512  ntrneineine1lem  44073  disjrnmpt2  45182  aiotavb  47091  dfatprc  47131  ndmafv2nrn  47223  nfunsnafv2  47226  oddneven  47645  usgrexmpl2trifr  48028