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 223	. 2 ⊢ (𝜑 ↔ 𝜒)
4	1, 3	xchnxbi 332	1 ⊢ (¬ 𝜒 ↔ 𝜓)

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  3ioran  1105  3ianor  1106  hadnot  1604  cadnot  1617  2exanali  1863  nelb  3195  nsspssun  4191  undif3  4224  2nreu  4375  intirr  6023  ordtri3or  6298  nf1const  7176  nf1oconst  7177  frxp  7967  ressuppssdif  8001  suppofssd  8019  domunfican  9087  ssfin4  10066  prinfzo0  13426  swrdnnn0nd  14369  swrdnd0  14370  lcmfunsnlem2lem1  16343  ncoprmlnprm  16432  prm23ge5  16516  smndex2dnrinv  18554  symgfix2  19024  gsumdixp  19848  cnfldfun  20609  symgmatr01lem  21802  ppttop  22157  zclmncvs  24312  mdegleb  25229  2lgslem3  26552  trlsegvdeg  28591  strlem1  30612  difrab2  30845  isarchi  31436  bnj1189  32989  dfacycgr1  33106  fmlasucdisj  33361  xpord3pred  33798  naddcllem  33831  dfon3  34194  wl-3xornot  35652  poimirlem18  35795  poimirlem21  35798  poimirlem30  35807  poimirlem31  35808  ftc1anclem3  35852  hdmaplem4  39788  mapdh9a  39803  ifpnot23  41085  ifpdfxor  41094  ifpnim1  41104  ifpnim2  41106  dfsucon  41130  ntrneineine1lem  41694  disjrnmpt2  42726  aiotavb  44582  dfatprc  44622  ndmafv2nrn  44714  nfunsnafv2  44717  oddneven  45096