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  1106  3ianor  1107  hadnot  1603  cadnot  1616  2exanali  1863  nabbib  3045  nelb  3231  nsspssun  4257  undif3  4290  2nreu  4441  intirr  6119  ordtri3or  6396  nf1const  7301  nf1oconst  7302  frxp  8111  ressuppssdif  8169  suppofssd  8187  naddcllem  8674  domunfican  9319  ssfin4  10304  prinfzo0  13670  swrdnnn0nd  14605  swrdnd0  14606  lcmfunsnlem2lem1  16574  ncoprmlnprm  16663  prm23ge5  16747  smndex2dnrinv  18795  symgfix2  19283  gsumdixp  20130  cnfldfun  20955  symgmatr01lem  22154  ppttop  22509  zclmncvs  24664  mdegleb  25581  2lgslem3  26904  trlsegvdeg  29477  strlem1  31498  difrab2  31733  isarchi  32323  bnj1189  34015  dfacycgr1  34130  fmlasucdisj  34385  dfon3  34859  wl-3xornot  36357  poimirlem18  36501  poimirlem21  36504  poimirlem30  36513  poimirlem31  36514  ftc1anclem3  36558  hdmaplem4  40640  mapdh9a  40655  onsupmaxb  41978  dflim5  42069  faosnf0.11b  42168  ifpnot23  42219  ifpdfxor  42228  ifpnim1  42238  ifpnim2  42240  dfsucon  42264  ntrneineine1lem  42825  disjrnmpt2  43876  aiotavb  45788  dfatprc  45828  ndmafv2nrn  45920  nfunsnafv2  45923  oddneven  46302