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  3028  nelb  3211  nsspssun  4227  undif3  4259  2nreu  4403  intirr  6079  ordtri3or  6352  nf1const  7261  nf1oconst  7262  frxp  8082  ressuppssdif  8141  suppofssd  8159  naddcllem  8617  domunfican  9248  ssfin4  10239  prinfzo0  13635  swrdnnn0nd  14597  swrdnd0  14598  lcmfunsnlem2lem1  16584  ncoprmlnprm  16674  prm23ge5  16762  smndex2dnrinv  18824  symgfix2  19330  gsumdixp  20239  cnfldfun  21310  cnfldfunOLD  21323  symgmatr01lem  22573  ppttop  22927  zclmncvs  25081  mdegleb  26002  2lgslem3  27348  trlsegvdeg  30206  strlem1  32229  difrab2  32477  isarchi  33151  bnj1189  34992  dfacycgr1  35124  fmlasucdisj  35379  dfon3  35873  wl-3xornot  37462  poimirlem18  37625  poimirlem21  37628  poimirlem30  37637  poimirlem31  37638  ftc1anclem3  37682  hdmaplem4  41761  mapdh9a  41776  onsupmaxb  43221  dflim5  43311  faosnf0.11b  43409  ifpnot23  43460  ifpdfxor  43469  ifpnim1  43479  ifpnim2  43481  dfsucon  43505  ntrneineine1lem  44066  disjrnmpt2  45175  aiotavb  47084  dfatprc  47124  ndmafv2nrn  47216  nfunsnafv2  47219  oddneven  47638  usgrexmpl2trifr  48021