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  1103  3ianor  1104  hadnot  1604  cadnot  1617  2exanali  1861  nsspssun  4184  undif3  4215  2nreu  4349  intirr  5945  ordtri3or  6191  nf1const  7038  nf1oconst  7039  frxp  7803  ressuppssdif  7834  suppofssd  7850  domunfican  8775  ssfin4  9721  prinfzo0  13071  swrdnnn0nd  14009  swrdnd0  14010  lcmfunsnlem2lem1  15972  ncoprmlnprm  16058  prm23ge5  16142  smndex2dnrinv  18072  symgfix2  18536  gsumdixp  19355  cnfldfunALT  20104  symgmatr01lem  21258  ppttop  21612  zclmncvs  23753  mdegleb  24665  2lgslem3  25988  trlsegvdeg  28012  strlem1  30033  difrab2  30268  isarchi  30861  bnj1189  32391  dfacycgr1  32504  fmlasucdisj  32759  dfon3  33466  wl-3xornot  34898  poimirlem18  35075  poimirlem21  35078  poimirlem30  35087  poimirlem31  35088  ftc1anclem3  35132  hdmaplem4  39070  mapdh9a  39085  ifpnot23  40186  ifpdfxor  40195  ifpnim1  40205  ifpnim2  40207  dfsucon  40231  ntrneineine1lem  40787  disjrnmpt2  41815  aiotavb  43647  dfatprc  43686  ndmafv2nrn  43778  nfunsnafv2  43781  oddneven  44162