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  1602  cadnot  1615  2exanali  1860  nabbib  3045  nelb  3234  nsspssun  4268  undif3  4300  2nreu  4444  intirr  6138  ordtri3or  6416  nf1const  7324  nf1oconst  7325  frxp  8151  ressuppssdif  8210  suppofssd  8228  naddcllem  8714  domunfican  9361  ssfin4  10350  prinfzo0  13738  swrdnnn0nd  14694  swrdnd0  14695  lcmfunsnlem2lem1  16675  ncoprmlnprm  16765  prm23ge5  16853  smndex2dnrinv  18928  symgfix2  19434  gsumdixp  20316  cnfldfun  21378  cnfldfunOLD  21391  symgmatr01lem  22659  ppttop  23014  zclmncvs  25182  mdegleb  26103  2lgslem3  27448  trlsegvdeg  30246  strlem1  32269  difrab2  32517  isarchi  33189  bnj1189  35023  dfacycgr1  35149  fmlasucdisj  35404  dfon3  35893  wl-3xornot  37482  poimirlem18  37645  poimirlem21  37648  poimirlem30  37657  poimirlem31  37658  ftc1anclem3  37702  hdmaplem4  41776  mapdh9a  41791  onsupmaxb  43251  dflim5  43342  faosnf0.11b  43440  ifpnot23  43491  ifpdfxor  43500  ifpnim1  43510  ifpnim2  43512  dfsucon  43536  ntrneineine1lem  44097  disjrnmpt2  45193  aiotavb  47102  dfatprc  47142  ndmafv2nrn  47234  nfunsnafv2  47237  oddneven  47631  usgrexmpl2trifr  47996