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  9222  ssfin4  10220  prinfzo0  13614  swrdnnn0nd  14580  swrdnd0  14581  lcmfunsnlem2lem1  16565  ncoprmlnprm  16655  prm23ge5  16743  smndex2dnrinv  18840  symgfix2  19345  gsumdixp  20254  cnfldfun  21323  cnfldfunOLD  21336  symgmatr01lem  22597  ppttop  22951  zclmncvs  25104  mdegleb  26025  2lgslem3  27371  trlsegvdeg  30302  strlem1  32325  difrab2  32572  isarchi  33264  bnj1189  35165  dfacycgr1  35338  fmlasucdisj  35593  dfon3  36084  wl-3xornot  37686  poimirlem18  37839  poimirlem21  37842  poimirlem30  37851  poimirlem31  37852  ftc1anclem3  37896  hdmaplem4  42034  mapdh9a  42049  onsupmaxb  43481  dflim5  43571  faosnf0.11b  43668  ifpnot23  43719  ifpdfxor  43728  ifpnim1  43738  ifpnim2  43740  dfsucon  43764  ntrneineine1lem  44325  disjrnmpt2  45432  aiotavb  47336  dfatprc  47376  ndmafv2nrn  47468  nfunsnafv2  47471  oddneven  47890  usgrexmpl2trifr  48283