Theorem xchnxbir 335

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

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  3ioran  1119  3ianor  1120  hadnot  1624  cadnot  1637  2exanali  1882  nabbib  3062  nelb  3240  nsspssun  4222  undif3  4254  2nreu  4400  intirr  6107  ordtri3or  6380  nf1const  7290  nf1oconst  7291  frxp  8108  ressuppssdif  8167  suppofssd  8185  naddcllem  8648  domunfican  9268  ssfin4  10269  prinfzo0  13706  swrdnnn0nd  14672  swrdnd0  14673  lcmfunsnlem2lem1  16674  ncoprmlnprm  16765  prm23ge5  16853  smndex2dnrinv  18954  symgfix2  19458  gsumdixp  20369  cnfldfun  21440  symgmatr01lem  22715  ppttop  23069  zclmncvs  25212  mdegleb  26126  2lgslem3  27470  trlsegvdeg  30431  strlem1  32455  difrab2  32699  isarchi  33364  bnj1189  35306  dfacycgr1  35499  fmlasucdisj  35754  dfon3  36245  wl-3xornot  37980  poimirlem18  38142  poimirlem21  38145  poimirlem30  38154  poimirlem31  38155  ftc1anclem3  38199  hdmaplem4  42403  mapdh9a  42418  onsupmaxb  43821  dflim5  43911  faosnf0.11b  44008  ifpnot23  44059  ifpdfxor  44068  ifpnim1  44078  ifpnim2  44080  dfsucon  44104  ntrneineine1lem  44665  disjrnmpt2  45771  aiotavb  47689  dfatprc  47729  ndmafv2nrn  47821  nfunsnafv2  47824  oddneven  48271  usgrexmpl2trifr  48664