Theorem xchnxbir 333

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

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  3ioran  1106  3ianor  1107  hadnot  1604  cadnot  1617  2exanali  1862  nabbib  3035  nelb  3213  nsspssun  4208  undif3  4240  2nreu  4384  intirr  6081  ordtri3or  6355  nf1const  7259  nf1oconst  7260  frxp  8076  ressuppssdif  8135  suppofssd  8153  naddcllem  8612  domunfican  9232  ssfin4  10232  prinfzo0  13653  swrdnnn0nd  14619  swrdnd0  14620  lcmfunsnlem2lem1  16607  ncoprmlnprm  16698  prm23ge5  16786  smndex2dnrinv  18886  symgfix2  19391  gsumdixp  20298  cnfldfun  21366  symgmatr01lem  22618  ppttop  22972  zclmncvs  25115  mdegleb  26029  2lgslem3  27367  trlsegvdeg  30297  strlem1  32321  difrab2  32567  isarchi  33243  bnj1189  35151  dfacycgr1  35326  fmlasucdisj  35581  dfon3  36072  wl-3xornot  37797  poimirlem18  37959  poimirlem21  37962  poimirlem30  37971  poimirlem31  37972  ftc1anclem3  38016  hdmaplem4  42220  mapdh9a  42235  onsupmaxb  43667  dflim5  43757  faosnf0.11b  43854  ifpnot23  43905  ifpdfxor  43914  ifpnim1  43924  ifpnim2  43926  dfsucon  43950  ntrneineine1lem  44511  disjrnmpt2  45618  aiotavb  47538  dfatprc  47578  ndmafv2nrn  47670  nfunsnafv2  47673  oddneven  48120  usgrexmpl2trifr  48513