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  1105  3ianor  1106  hadnot  1603  cadnot  1616  2exanali  1861  nabbib  3035  nelb  3212  nsspssun  4220  undif3  4252  2nreu  4396  intirr  6075  ordtri3or  6349  nf1const  7250  nf1oconst  7251  frxp  8068  ressuppssdif  8127  suppofssd  8145  naddcllem  8604  domunfican  9224  ssfin4  10222  prinfzo0  13616  swrdnnn0nd  14582  swrdnd0  14583  lcmfunsnlem2lem1  16567  ncoprmlnprm  16657  prm23ge5  16745  smndex2dnrinv  18842  symgfix2  19347  gsumdixp  20256  cnfldfun  21325  cnfldfunOLD  21338  symgmatr01lem  22599  ppttop  22953  zclmncvs  25106  mdegleb  26027  2lgslem3  27373  trlsegvdeg  30304  strlem1  32327  difrab2  32574  isarchi  33266  bnj1189  35167  dfacycgr1  35340  fmlasucdisj  35595  dfon3  36086  wl-3xornot  37688  poimirlem18  37841  poimirlem21  37844  poimirlem30  37853  poimirlem31  37854  ftc1anclem3  37898  hdmaplem4  42056  mapdh9a  42071  onsupmaxb  43502  dflim5  43592  faosnf0.11b  43689  ifpnot23  43740  ifpdfxor  43749  ifpnim1  43759  ifpnim2  43761  dfsucon  43785  ntrneineine1lem  44346  disjrnmpt2  45453  aiotavb  47357  dfatprc  47397  ndmafv2nrn  47489  nfunsnafv2  47492  oddneven  47911  usgrexmpl2trifr  48304