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  1108  3ianor  1109  hadnot  1609  cadnot  1622  2exanali  1868  nsspssun  4172  undif3  4205  2nreu  4356  intirr  5983  ordtri3or  6245  nf1const  7114  nf1oconst  7115  frxp  7893  ressuppssdif  7927  suppofssd  7945  domunfican  8944  ssfin4  9924  prinfzo0  13281  swrdnnn0nd  14221  swrdnd0  14222  lcmfunsnlem2lem1  16195  ncoprmlnprm  16284  prm23ge5  16368  smndex2dnrinv  18342  symgfix2  18808  gsumdixp  19627  cnfldfunALT  20376  symgmatr01lem  21550  ppttop  21904  zclmncvs  24045  mdegleb  24962  2lgslem3  26285  trlsegvdeg  28310  strlem1  30331  difrab2  30564  isarchi  31155  bnj1189  32702  dfacycgr1  32819  fmlasucdisj  33074  xpord3pred  33535  naddcllem  33568  dfon3  33931  wl-3xornot  35389  poimirlem18  35532  poimirlem21  35535  poimirlem30  35544  poimirlem31  35545  ftc1anclem3  35589  hdmaplem4  39525  mapdh9a  39540  ifpnot23  40770  ifpdfxor  40779  ifpnim1  40789  ifpnim2  40791  dfsucon  40815  ntrneineine1lem  41371  disjrnmpt2  42399  aiotavb  44254  dfatprc  44294  ndmafv2nrn  44386  nfunsnafv2  44389  oddneven  44769