Theorem xchnxbir 334

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

Syntax hints:  ¬ wn 3   ↔ wb 207

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 208

This theorem is referenced by:  3ioran  1111  3ianor  1112  hadnot  1609  cadnot  1622  2exanali  1867  nabbib  3037  nelb  3215  nsspssun  4197  undif3  4229  2nreu  4373  intirr  6069  ordtri3or  6343  nf1const  7249  nf1oconst  7250  frxp  8067  ressuppssdif  8126  suppofssd  8144  naddcllem  8603  domunfican  9223  ssfin4  10224  prinfzo0  13645  swrdnnn0nd  14611  swrdnd0  14612  lcmfunsnlem2lem1  16599  ncoprmlnprm  16690  prm23ge5  16778  smndex2dnrinv  18878  symgfix2  19383  gsumdixp  20290  cnfldfun  21362  symgmatr01lem  22637  ppttop  22991  zclmncvs  25134  mdegleb  26048  2lgslem3  27386  trlsegvdeg  30316  strlem1  32340  difrab2  32586  isarchi  33264  bnj1189  35200  dfacycgr1  35381  fmlasucdisj  35636  dfon3  36127  wl-3xornot  37852  poimirlem18  38014  poimirlem21  38017  poimirlem30  38026  poimirlem31  38027  ftc1anclem3  38071  hdmaplem4  42275  mapdh9a  42290  onsupmaxb  43693  dflim5  43783  faosnf0.11b  43880  ifpnot23  43931  ifpdfxor  43940  ifpnim1  43950  ifpnim2  43952  dfsucon  43976  ntrneineine1lem  44537  disjrnmpt2  45643  aiotavb  47561  dfatprc  47601  ndmafv2nrn  47693  nfunsnafv2  47696  oddneven  48143  usgrexmpl2trifr  48536