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 223	. 2 ⊢ (𝜑 ↔ 𝜒)
4	1, 3	xchnxbi 332	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  1107  3ianor  1108  hadnot  1604  cadnot  1617  2exanali  1864  nabbib  3046  nelb  3232  nsspssun  4258  undif3  4291  2nreu  4442  intirr  6120  ordtri3or  6397  nf1const  7302  nf1oconst  7303  frxp  8112  ressuppssdif  8170  suppofssd  8188  naddcllem  8675  domunfican  9320  ssfin4  10305  prinfzo0  13671  swrdnnn0nd  14606  swrdnd0  14607  lcmfunsnlem2lem1  16575  ncoprmlnprm  16664  prm23ge5  16748  smndex2dnrinv  18796  symgfix2  19284  gsumdixp  20131  cnfldfun  20956  symgmatr01lem  22155  ppttop  22510  zclmncvs  24665  mdegleb  25582  2lgslem3  26907  trlsegvdeg  29480  strlem1  31503  difrab2  31738  isarchi  32328  bnj1189  34020  dfacycgr1  34135  fmlasucdisj  34390  dfon3  34864  wl-3xornot  36362  poimirlem18  36506  poimirlem21  36509  poimirlem30  36518  poimirlem31  36519  ftc1anclem3  36563  hdmaplem4  40645  mapdh9a  40660  onsupmaxb  41988  dflim5  42079  faosnf0.11b  42178  ifpnot23  42229  ifpdfxor  42238  ifpnim1  42248  ifpnim2  42250  dfsucon  42274  ntrneineine1lem  42835  disjrnmpt2  43886  aiotavb  45798  dfatprc  45838  ndmafv2nrn  45930  nfunsnafv2  45933  oddneven  46312