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  1603  cadnot  1616  2exanali  1861  nabbib  3033  nelb  3210  nsspssun  4218  undif3  4250  2nreu  4394  intirr  6073  ordtri3or  6347  nf1const  7248  nf1oconst  7249  frxp  8066  ressuppssdif  8125  suppofssd  8143  naddcllem  8602  domunfican  9220  ssfin4  10218  prinfzo0  13612  swrdnnn0nd  14578  swrdnd0  14579  lcmfunsnlem2lem1  16563  ncoprmlnprm  16653  prm23ge5  16741  smndex2dnrinv  18838  symgfix2  19343  gsumdixp  20252  cnfldfun  21321  cnfldfunOLD  21334  symgmatr01lem  22595  ppttop  22949  zclmncvs  25102  mdegleb  26023  2lgslem3  27369  trlsegvdeg  30251  strlem1  32274  difrab2  32521  isarchi  33213  bnj1189  35114  dfacycgr1  35287  fmlasucdisj  35542  dfon3  36033  wl-3xornot  37625  poimirlem18  37778  poimirlem21  37781  poimirlem30  37790  poimirlem31  37791  ftc1anclem3  37835  hdmaplem4  41973  mapdh9a  41988  onsupmaxb  43423  dflim5  43513  faosnf0.11b  43610  ifpnot23  43661  ifpdfxor  43670  ifpnim1  43680  ifpnim2  43682  dfsucon  43706  ntrneineine1lem  44267  disjrnmpt2  45374  aiotavb  47278  dfatprc  47318  ndmafv2nrn  47410  nfunsnafv2  47413  oddneven  47832  usgrexmpl2trifr  48225