Theorem xchnxbir 336

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 227	. 2 ⊢ (𝜑 ↔ 𝜒)
4	1, 3	xchnxbi 335	1 ⊢ (¬ 𝜒 ↔ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3ioran  1123  3ianor  1124  hadnot  1631  cadnot  1647  2exanali  1892  nabbib  3064  nelb  3242  nsspssun  4216  undif3  4248  2nreu  4405  intirr  6118  ordtri3or  6402  fvtp0  7216  nf1const  7322  nf1oconst  7323  frxp  8151  ressuppssdif  8216  suppofssd  8234  naddcllem  8699  domunfican  9327  ssfin4  10401  prinfzo0  13846  swrdnnn0nd  14820  swrdnd0  14821  lcmfunsnlem2lem1  16828  ncoprmlnprm  16919  prm23ge5  17008  smndex2dnrinv  19129  symgfix2  19645  gsumdixp  20563  isfieldidl  21555  cnfldfun  21707  symgmatr01lem  22983  ppttop  23340  zclmncvs  25484  mdegleb  26397  2lgslem3  27746  dfacycgr1  30765  trlsegvdeg  30843  strlem1  32867  difrab2  33151  isarchi  33799  bnj1189  35695  fmlasucdisj  36288  dfon3  36787  wl-3xornot  38550  poimirlem18  38702  poimirlem21  38705  poimirlem30  38714  poimirlem31  38715  ftc1anclem3  38759  hdmaplem4  42977  mapdh9a  42992  onsupmaxb  44387  dflim5  44477  faosnf0.11b  44574  ifpnot23  44625  ifpdfxor  44634  ifpnim1  44644  ifpnim2  44646  dfsucon  44670  ntrneineine1lem  45230  disjrnmpt2  46348  aiotavb  48305  dfatprc  48345  ndmafv2nrn  48437  nfunsnafv2  48440  oddneven  48887  usgrexmpl2trifr  49280