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  3036  nelb  3214  nsspssun  4209  undif3  4241  2nreu  4385  intirr  6077  ordtri3or  6351  nf1const  7254  nf1oconst  7255  frxp  8071  ressuppssdif  8130  suppofssd  8148  naddcllem  8607  domunfican  9227  ssfin4  10227  prinfzo0  13648  swrdnnn0nd  14614  swrdnd0  14615  lcmfunsnlem2lem1  16602  ncoprmlnprm  16693  prm23ge5  16781  smndex2dnrinv  18881  symgfix2  19386  gsumdixp  20293  cnfldfun  21362  cnfldfunOLD  21375  symgmatr01lem  22632  ppttop  22986  zclmncvs  25129  mdegleb  26043  2lgslem3  27385  trlsegvdeg  30316  strlem1  32340  difrab2  32586  isarchi  33262  bnj1189  35171  dfacycgr1  35346  fmlasucdisj  35601  dfon3  36092  wl-3xornot  37815  poimirlem18  37977  poimirlem21  37980  poimirlem30  37989  poimirlem31  37990  ftc1anclem3  38034  hdmaplem4  42238  mapdh9a  42253  onsupmaxb  43689  dflim5  43779  faosnf0.11b  43876  ifpnot23  43927  ifpdfxor  43936  ifpnim1  43946  ifpnim2  43948  dfsucon  43972  ntrneineine1lem  44533  disjrnmpt2  45640  aiotavb  47554  dfatprc  47594  ndmafv2nrn  47686  nfunsnafv2  47689  oddneven  48136  usgrexmpl2trifr  48529