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

Syntax hints:  ¬ wn 3   ↔ wb 195

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 196

This theorem is referenced by:  3ioran  1049  hadnot  1532  cadnot  1545  nsspssun  3819  undif3  3847  undif3OLD  3848  intirr  5433  ordtri3or  5672  frxp  7174  ressuppssdif  7203  domunfican  8118  ssfin4  9015  lcmfunsnlem2lem1  15189  ncoprmlnprm  15274  prm23ge5  15358  symgfix2  17659  gsumdixp  18432  symgmatr01lem  20278  ppttop  20621  zclmncvs  22756  mdegleb  23628  2lgslem3  24929  strlem1  28493  isarchi  29067  bnj1189  30331  dfon3  31169  poimirlem18  32597  poimirlem21  32600  poimirlem30  32609  poimirlem31  32610  ftc1anclem3  32657  hdmaplem4  36081  mapdh9a  36097  ifpnot23  36842  ifpdfxor  36851  ifpnim1  36861  ifpnim2  36863  relintabex  36906  ntrneineine1lem  37402  2exanali  37609  oddneven  40095  prinfzo0  40363  trlsegvdeg  41395