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  3205  nsspssun  4219  undif3  4251  2nreu  4395  intirr  6067  ordtri3or  6339  nf1const  7241  nf1oconst  7242  frxp  8059  ressuppssdif  8118  suppofssd  8136  naddcllem  8594  domunfican  9211  ssfin4  10204  prinfzo0  13601  swrdnnn0nd  14563  swrdnd0  14564  lcmfunsnlem2lem1  16549  ncoprmlnprm  16639  prm23ge5  16727  smndex2dnrinv  18789  symgfix2  19295  gsumdixp  20204  cnfldfun  21275  cnfldfunOLD  21288  symgmatr01lem  22538  ppttop  22892  zclmncvs  25046  mdegleb  25967  2lgslem3  27313  trlsegvdeg  30171  strlem1  32194  difrab2  32442  isarchi  33125  bnj1189  34982  dfacycgr1  35127  fmlasucdisj  35382  dfon3  35876  wl-3xornot  37465  poimirlem18  37628  poimirlem21  37631  poimirlem30  37640  poimirlem31  37641  ftc1anclem3  37685  hdmaplem4  41763  mapdh9a  41778  onsupmaxb  43222  dflim5  43312  faosnf0.11b  43410  ifpnot23  43461  ifpdfxor  43470  ifpnim1  43480  ifpnim2  43482  dfsucon  43506  ntrneineine1lem  44067  disjrnmpt2  45176  aiotavb  47084  dfatprc  47124  ndmafv2nrn  47216  nfunsnafv2  47219  oddneven  47638  usgrexmpl2trifr  48031