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  1632  cadnot  1645  2exanali  1890  nabbib  3063  nelb  3241  nsspssun  4221  undif3  4253  2nreu  4409  intirr  6118  ordtri3or  6393  nf1const  7302  nf1oconst  7303  frxp  8118  ressuppssdif  8177  suppofssd  8195  naddcllem  8658  domunfican  9277  ssfin4  10298  prinfzo0  13732  swrdnnn0nd  14699  swrdnd0  14700  lcmfunsnlem2lem1  16700  ncoprmlnprm  16791  prm23ge5  16879  smndex2dnrinv  18981  symgfix2  19490  gsumdixp  20405  isfieldidl  21395  cnfldfun  21545  symgmatr01lem  22819  ppttop  23173  zclmncvs  25316  mdegleb  26230  2lgslem3  27577  trlsegvdeg  30587  strlem1  32611  difrab2  32853  isarchi  33511  bnj1189  35406  dfacycgr1  35644  fmlasucdisj  35899  dfon3  36390  wl-3xornot  38155  poimirlem18  38317  poimirlem21  38320  poimirlem30  38329  poimirlem31  38330  ftc1anclem3  38374  hdmaplem4  42576  mapdh9a  42591  onsupmaxb  43994  dflim5  44084  faosnf0.11b  44181  ifpnot23  44232  ifpdfxor  44241  ifpnim1  44251  ifpnim2  44253  dfsucon  44277  ntrneineine1lem  44838  disjrnmpt2  45934  aiotavb  47855  dfatprc  47895  ndmafv2nrn  47987  nfunsnafv2  47990  oddneven  48437  usgrexmpl2trifr  48830