Theorem xchnxbir 332

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

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  3ioran  1104  3ianor  1105  hadnot  1605  cadnot  1618  2exanali  1864  nelb  3194  nsspssun  4188  undif3  4221  2nreu  4372  intirr  6012  ordtri3or  6283  nf1const  7156  nf1oconst  7157  frxp  7938  ressuppssdif  7972  suppofssd  7990  domunfican  9017  ssfin4  9997  prinfzo0  13354  swrdnnn0nd  14297  swrdnd0  14298  lcmfunsnlem2lem1  16271  ncoprmlnprm  16360  prm23ge5  16444  smndex2dnrinv  18469  symgfix2  18939  gsumdixp  19763  cnfldfunALT  20523  symgmatr01lem  21710  ppttop  22065  zclmncvs  24217  mdegleb  25134  2lgslem3  26457  trlsegvdeg  28492  strlem1  30513  difrab2  30746  isarchi  31338  bnj1189  32889  dfacycgr1  33006  fmlasucdisj  33261  xpord3pred  33725  naddcllem  33758  dfon3  34121  wl-3xornot  35579  poimirlem18  35722  poimirlem21  35725  poimirlem30  35734  poimirlem31  35735  ftc1anclem3  35779  hdmaplem4  39715  mapdh9a  39730  ifpnot23  40983  ifpdfxor  40992  ifpnim1  41002  ifpnim2  41004  dfsucon  41028  ntrneineine1lem  41583  disjrnmpt2  42615  aiotavb  44469  dfatprc  44509  ndmafv2nrn  44601  nfunsnafv2  44604  oddneven  44984