Theorem xchnxbir 325

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

Syntax hints:  ¬ wn 3   ↔ wb 198

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 199

This theorem is referenced by:  3ioran  1135  3ianor  1136  hadnot  1715  cadnot  1728  nsspssun  4089  undif3  4120  intirr  5760  ordtri3or  5999  frxp  7556  ressuppssdif  7585  domunfican  8508  ssfin4  9454  prinfzo0  12809  swrdnnn0nd  13728  swrdnd0  13729  lcmfunsnlem2lem1  15731  ncoprmlnprm  15814  prm23ge5  15898  symgfix2  18193  gsumdixp  18970  cnfldfunALT  20126  symgmatr01lem  20835  ppttop  21189  zclmncvs  23324  mdegleb  24230  2lgslem3  25549  trlsegvdeg  27600  strlem1  29660  isarchi  30277  bnj1189  31619  dfon3  32533  poimirlem18  33970  poimirlem21  33973  poimirlem30  33982  poimirlem31  33983  ftc1anclem3  34029  hdmaplem4  37848  mapdh9a  37863  ifpnot23  38664  ifpdfxor  38673  ifpnim1  38683  ifpnim2  38685  relintabex  38727  ntrneineine1lem  39221  2exanali  39426  aiotavb  41985  dfatprc  42030  ndmafv2nrn  42122  nfunsnafv2  42125  oddneven  42405