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  3031  nelb  3208  nsspssun  4215  undif3  4247  2nreu  4391  intirr  6064  ordtri3or  6338  nf1const  7238  nf1oconst  7239  frxp  8056  ressuppssdif  8115  suppofssd  8133  naddcllem  8591  domunfican  9206  ssfin4  10201  prinfzo0  13598  swrdnnn0nd  14564  swrdnd0  14565  lcmfunsnlem2lem1  16549  ncoprmlnprm  16639  prm23ge5  16727  smndex2dnrinv  18823  symgfix2  19328  gsumdixp  20237  cnfldfun  21305  cnfldfunOLD  21318  symgmatr01lem  22568  ppttop  22922  zclmncvs  25075  mdegleb  25996  2lgslem3  27342  trlsegvdeg  30207  strlem1  32230  difrab2  32477  isarchi  33151  bnj1189  35021  dfacycgr1  35188  fmlasucdisj  35443  dfon3  35934  wl-3xornot  37525  poimirlem18  37688  poimirlem21  37691  poimirlem30  37700  poimirlem31  37701  ftc1anclem3  37745  hdmaplem4  41883  mapdh9a  41898  onsupmaxb  43342  dflim5  43432  faosnf0.11b  43530  ifpnot23  43581  ifpdfxor  43590  ifpnim1  43600  ifpnim2  43602  dfsucon  43626  ntrneineine1lem  44187  disjrnmpt2  45295  aiotavb  47200  dfatprc  47240  ndmafv2nrn  47332  nfunsnafv2  47335  oddneven  47754  usgrexmpl2trifr  48147