Theorem xchnxbir 333

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

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  3ioran  1105  3ianor  1106  hadnot  1602  cadnot  1615  2exanali  1860  nabbib  3029  nelb  3214  nsspssun  4234  undif3  4266  2nreu  4410  intirr  6094  ordtri3or  6367  nf1const  7282  nf1oconst  7283  frxp  8108  ressuppssdif  8167  suppofssd  8185  naddcllem  8643  domunfican  9279  ssfin4  10270  prinfzo0  13666  swrdnnn0nd  14628  swrdnd0  14629  lcmfunsnlem2lem1  16615  ncoprmlnprm  16705  prm23ge5  16793  smndex2dnrinv  18849  symgfix2  19353  gsumdixp  20235  cnfldfun  21285  cnfldfunOLD  21298  symgmatr01lem  22547  ppttop  22901  zclmncvs  25055  mdegleb  25976  2lgslem3  27322  trlsegvdeg  30163  strlem1  32186  difrab2  32434  isarchi  33143  bnj1189  35006  dfacycgr1  35138  fmlasucdisj  35393  dfon3  35887  wl-3xornot  37476  poimirlem18  37639  poimirlem21  37642  poimirlem30  37651  poimirlem31  37652  ftc1anclem3  37696  hdmaplem4  41775  mapdh9a  41790  onsupmaxb  43235  dflim5  43325  faosnf0.11b  43423  ifpnot23  43474  ifpdfxor  43483  ifpnim1  43493  ifpnim2  43495  dfsucon  43519  ntrneineine1lem  44080  disjrnmpt2  45189  aiotavb  47095  dfatprc  47135  ndmafv2nrn  47227  nfunsnafv2  47230  oddneven  47649  usgrexmpl2trifr  48032