Theorem xchnxbir 333

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

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  3ioran  1105  3ianor  1106  hadnot  1602  cadnot  1615  2exanali  1860  nabbib  3035  nelb  3218  nsspssun  4243  undif3  4275  2nreu  4419  intirr  6107  ordtri3or  6384  nf1const  7296  nf1oconst  7297  frxp  8123  ressuppssdif  8182  suppofssd  8200  naddcllem  8686  domunfican  9331  ssfin4  10322  prinfzo0  13713  swrdnnn0nd  14672  swrdnd0  14673  lcmfunsnlem2lem1  16655  ncoprmlnprm  16745  prm23ge5  16833  smndex2dnrinv  18891  symgfix2  19395  gsumdixp  20277  cnfldfun  21327  cnfldfunOLD  21340  symgmatr01lem  22589  ppttop  22943  zclmncvs  25098  mdegleb  26019  2lgslem3  27365  trlsegvdeg  30154  strlem1  32177  difrab2  32425  isarchi  33126  bnj1189  34986  dfacycgr1  35112  fmlasucdisj  35367  dfon3  35856  wl-3xornot  37445  poimirlem18  37608  poimirlem21  37611  poimirlem30  37620  poimirlem31  37621  ftc1anclem3  37665  hdmaplem4  41739  mapdh9a  41754  onsupmaxb  43210  dflim5  43300  faosnf0.11b  43398  ifpnot23  43449  ifpdfxor  43458  ifpnim1  43468  ifpnim2  43470  dfsucon  43494  ntrneineine1lem  44055  disjrnmpt2  45160  aiotavb  47067  dfatprc  47107  ndmafv2nrn  47199  nfunsnafv2  47202  oddneven  47606  usgrexmpl2trifr  47989