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  1599  cadnot  1612  2exanali  1859  nabbib  3051  nelb  3240  nsspssun  4287  undif3  4319  2nreu  4467  intirr  6150  ordtri3or  6427  nf1const  7340  nf1oconst  7341  frxp  8167  ressuppssdif  8226  suppofssd  8244  naddcllem  8732  domunfican  9389  ssfin4  10379  prinfzo0  13755  swrdnnn0nd  14704  swrdnd0  14705  lcmfunsnlem2lem1  16685  ncoprmlnprm  16775  prm23ge5  16862  smndex2dnrinv  18950  symgfix2  19458  gsumdixp  20342  cnfldfun  21401  cnfldfunOLD  21414  symgmatr01lem  22680  ppttop  23035  zclmncvs  25201  mdegleb  26123  2lgslem3  27466  trlsegvdeg  30259  strlem1  32282  difrab2  32526  isarchi  33162  bnj1189  34985  dfacycgr1  35112  fmlasucdisj  35367  dfon3  35856  wl-3xornot  37447  poimirlem18  37598  poimirlem21  37601  poimirlem30  37610  poimirlem31  37611  ftc1anclem3  37655  hdmaplem4  41731  mapdh9a  41746  onsupmaxb  43200  dflim5  43291  faosnf0.11b  43389  ifpnot23  43440  ifpdfxor  43449  ifpnim1  43459  ifpnim2  43461  dfsucon  43485  ntrneineine1lem  44046  disjrnmpt2  45095  aiotavb  47005  dfatprc  47045  ndmafv2nrn  47137  nfunsnafv2  47140  oddneven  47518  usgrexmpl2trifr  47852