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  3065  nelb  3243  nsspssun  4221  undif3  4253  2nreu  4409  intirr  6120  ordtri3or  6397  fvtp0  7205  nf1const  7311  nf1oconst  7312  frxp  8128  ressuppssdif  8187  suppofssd  8205  naddcllem  8668  domunfican  9288  ssfin4  10309  prinfzo0  13748  swrdnnn0nd  14720  swrdnd0  14721  lcmfunsnlem2lem1  16722  ncoprmlnprm  16813  prm23ge5  16901  smndex2dnrinv  19018  symgfix2  19534  gsumdixp  20450  isfieldidl  21440  cnfldfun  21590  symgmatr01lem  22864  ppttop  23218  zclmncvs  25362  mdegleb  26276  2lgslem3  27623  trlsegvdeg  30653  strlem1  32677  difrab2  32919  isarchi  33570  bnj1189  35466  dfacycgr1  35677  fmlasucdisj  35932  dfon3  36423  wl-3xornot  38188  poimirlem18  38350  poimirlem21  38353  poimirlem30  38362  poimirlem31  38363  ftc1anclem3  38407  hdmaplem4  42610  mapdh9a  42625  onsupmaxb  44043  dflim5  44133  faosnf0.11b  44230  ifpnot23  44281  ifpdfxor  44290  ifpnim1  44300  ifpnim2  44302  dfsucon  44326  ntrneineine1lem  44887  disjrnmpt2  45983  aiotavb  47904  dfatprc  47944  ndmafv2nrn  48036  nfunsnafv2  48039  oddneven  48486  usgrexmpl2trifr  48879