Theorem xchnxbir 332

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 331	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  1104  3ianor  1105  hadnot  1601  cadnot  1614  2exanali  1861  nabbib  3043  nelb  3229  nsspssun  4256  undif3  4289  2nreu  4440  intirr  6118  ordtri3or  6395  nf1const  7304  nf1oconst  7305  frxp  8114  ressuppssdif  8172  suppofssd  8190  naddcllem  8677  domunfican  9322  ssfin4  10307  prinfzo0  13675  swrdnnn0nd  14610  swrdnd0  14611  lcmfunsnlem2lem1  16579  ncoprmlnprm  16668  prm23ge5  16752  smndex2dnrinv  18832  symgfix2  19325  gsumdixp  20207  cnfldfun  21156  symgmatr01lem  22375  ppttop  22730  zclmncvs  24896  mdegleb  25817  2lgslem3  27143  trlsegvdeg  29747  strlem1  31770  difrab2  32005  isarchi  32598  bnj1189  34318  dfacycgr1  34433  fmlasucdisj  34688  dfon3  35168  gg-cnfldfun  35483  wl-3xornot  36665  poimirlem18  36809  poimirlem21  36812  poimirlem30  36821  poimirlem31  36822  ftc1anclem3  36866  hdmaplem4  40948  mapdh9a  40963  onsupmaxb  42290  dflim5  42381  faosnf0.11b  42480  ifpnot23  42531  ifpdfxor  42540  ifpnim1  42550  ifpnim2  42552  dfsucon  42576  ntrneineine1lem  43137  disjrnmpt2  44185  aiotavb  46096  dfatprc  46136  ndmafv2nrn  46228  nfunsnafv2  46231  oddneven  46610