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  3061  nelb  3239  nsspssun  4214  undif3  4246  2nreu  4402  intirr  6112  ordtri3or  6395  fvtp0  7206  nf1const  7312  nf1oconst  7313  frxp  8138  ressuppssdif  8202  suppofssd  8220  naddcllem  8685  domunfican  9313  ssfin4  10388  prinfzo0  13833  swrdnnn0nd  14806  swrdnd0  14807  lcmfunsnlem2lem1  16813  ncoprmlnprm  16904  prm23ge5  16993  smndex2dnrinv  19114  symgfix2  19630  gsumdixp  20548  isfieldidl  21540  cnfldfun  21692  symgmatr01lem  22968  ppttop  23325  zclmncvs  25469  mdegleb  26382  2lgslem3  27731  dfacycgr1  30750  trlsegvdeg  30828  strlem1  32852  difrab2  33094  isarchi  33743  bnj1189  35639  fmlasucdisj  36164  dfon3  36654  wl-3xornot  38404  poimirlem18  38556  poimirlem21  38559  poimirlem30  38568  poimirlem31  38569  ftc1anclem3  38613  hdmaplem4  42831  mapdh9a  42846  onsupmaxb  44240  dflim5  44330  faosnf0.11b  44427  ifpnot23  44478  ifpdfxor  44487  ifpnim1  44497  ifpnim2  44499  dfsucon  44523  ntrneineine1lem  45083  disjrnmpt2  46202  aiotavb  48159  dfatprc  48199  ndmafv2nrn  48291  nfunsnafv2  48294  oddneven  48741  usgrexmpl2trifr  49134