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 ⊢ (¬ 𝜒 ↔ 𝜓)

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  3ioran  1121  3ianor  1122  hadnot  1629  cadnot  1642  2exanali  1887  nabbib  3069  nelb  3247  nsspssun  4229  undif3  4261  2nreu  4415  intirr  6119  ordtri3or  6394  nf1const  7303  nf1oconst  7304  frxp  8122  ressuppssdif  8181  suppofssd  8199  naddcllem  8662  domunfican  9281  ssfin4  10294  prinfzo0  13727  swrdnnn0nd  14694  swrdnd0  14695  lcmfunsnlem2lem1  16696  ncoprmlnprm  16787  prm23ge5  16875  smndex2dnrinv  18977  symgfix2  19486  gsumdixp  20400  cnfldfun  21505  symgmatr01lem  22779  ppttop  23133  zclmncvs  25276  mdegleb  26190  2lgslem3  27534  trlsegvdeg  30519  strlem1  32543  difrab2  32785  isarchi  33443  bnj1189  35342  dfacycgr1  35569  fmlasucdisj  35824  dfon3  36315  wl-3xornot  38049  poimirlem18  38211  poimirlem21  38214  poimirlem30  38223  poimirlem31  38224  ftc1anclem3  38268  hdmaplem4  42472  mapdh9a  42487  onsupmaxb  43892  dflim5  43982  faosnf0.11b  44079  ifpnot23  44130  ifpdfxor  44139  ifpnim1  44149  ifpnim2  44151  dfsucon  44175  ntrneineine1lem  44736  disjrnmpt2  45832  aiotavb  47750  dfatprc  47790  ndmafv2nrn  47882  nfunsnafv2  47885  oddneven  48332  usgrexmpl2trifr  48725