Theorem xchnxbir 322

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

Syntax hints:  ¬ wn 3   ↔ wb 196

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 197

This theorem is referenced by:  3ioran  1095  3ianor  1096  hadnot  1689  cadnot  1702  nsspssun  4006  undif3  4037  intirr  5654  ordtri3or  5897  frxp  7442  ressuppssdif  7471  domunfican  8393  ssfin4  9338  prinfzo0  12715  lcmfunsnlem2lem1  15559  ncoprmlnprm  15643  prm23ge5  15727  symgfix2  18043  gsumdixp  18817  cnfldfunALT  19974  symgmatr01lem  20678  ppttop  21032  zclmncvs  23167  mdegleb  24044  2lgslem3  25350  trlsegvdeg  27407  strlem1  29449  isarchi  30076  bnj1189  31415  dfon3  32336  poimirlem18  33760  poimirlem21  33763  poimirlem30  33772  poimirlem31  33773  ftc1anclem3  33819  hdmaplem4  37584  mapdh9a  37599  ifpnot23  38349  ifpdfxor  38358  ifpnim1  38368  ifpnim2  38370  relintabex  38413  ntrneineine1lem  38908  2exanali  39113  oddneven  42082