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  4222  undif3  4254  2nreu  4398  intirr  6085  ordtri3or  6359  nf1const  7262  nf1oconst  7263  frxp  8080  ressuppssdif  8139  suppofssd  8157  naddcllem  8616  domunfican  9236  ssfin4  10234  prinfzo0  13628  swrdnnn0nd  14594  swrdnd0  14595  lcmfunsnlem2lem1  16579  ncoprmlnprm  16669  prm23ge5  16757  smndex2dnrinv  18857  symgfix2  19362  gsumdixp  20271  cnfldfun  21340  cnfldfunOLD  21353  symgmatr01lem  22614  ppttop  22968  zclmncvs  25121  mdegleb  26042  2lgslem3  27388  trlsegvdeg  30320  strlem1  32344  difrab2  32590  isarchi  33282  bnj1189  35191  dfacycgr1  35366  fmlasucdisj  35621  dfon3  36112  wl-3xornot  37763  poimirlem18  37918  poimirlem21  37921  poimirlem30  37930  poimirlem31  37931  ftc1anclem3  37975  hdmaplem4  42179  mapdh9a  42194  onsupmaxb  43625  dflim5  43715  faosnf0.11b  43812  ifpnot23  43863  ifpdfxor  43872  ifpnim1  43882  ifpnim2  43884  dfsucon  43908  ntrneineine1lem  44469  disjrnmpt2  45576  aiotavb  47479  dfatprc  47519  ndmafv2nrn  47611  nfunsnafv2  47614  oddneven  48033  usgrexmpl2trifr  48426