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  1648  2exanali  1893  nabbib  3060  nelb  3238  nsspssun  4214  undif3  4246  2nreu  4402  intirr  6113  ordtri3or  6391  fvtp0  7201  nf1const  7307  nf1oconst  7308  frxp  8126  ressuppssdif  8185  suppofssd  8203  naddcllem  8668  domunfican  9295  ssfin4  10334  prinfzo0  13776  swrdnnn0nd  14748  swrdnd0  14749  lcmfunsnlem2lem1  16750  ncoprmlnprm  16841  prm23ge5  16929  smndex2dnrinv  19050  symgfix2  19566  gsumdixp  20484  isfieldidl  21476  cnfldfun  21628  symgmatr01lem  22904  ppttop  23261  zclmncvs  25405  mdegleb  26318  2lgslem3  27669  dfacycgr1  30658  trlsegvdeg  30736  strlem1  32760  difrab2  33002  isarchi  33651  bnj1189  35548  fmlasucdisj  36008  dfon3  36499  wl-3xornot  38249  poimirlem18  38401  poimirlem21  38404  poimirlem30  38413  poimirlem31  38414  ftc1anclem3  38458  hdmaplem4  42661  mapdh9a  42676  onsupmaxb  44094  dflim5  44184  faosnf0.11b  44281  ifpnot23  44332  ifpdfxor  44341  ifpnim1  44351  ifpnim2  44353  dfsucon  44377  ntrneineine1lem  44938  disjrnmpt2  46034  aiotavb  47992  dfatprc  48032  ndmafv2nrn  48124  nfunsnafv2  48127  oddneven  48574  usgrexmpl2trifr  48967