Theorem xchnxbir 335

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

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  3ioran  1102  3ianor  1103  hadnot  1603  cadnot  1616  2exanali  1860  nsspssun  4234  undif3  4265  2nreu  4393  intirr  5978  ordtri3or  6223  nf1const  7059  nf1oconst  7060  frxp  7820  ressuppssdif  7851  suppofssd  7867  domunfican  8791  ssfin4  9732  prinfzo0  13077  swrdnnn0nd  14018  swrdnd0  14019  lcmfunsnlem2lem1  15982  ncoprmlnprm  16068  prm23ge5  16152  smndex2dnrinv  18080  symgfix2  18544  gsumdixp  19359  cnfldfunALT  20558  symgmatr01lem  21262  ppttop  21615  zclmncvs  23752  mdegleb  24658  2lgslem3  25980  trlsegvdeg  28006  strlem1  30027  difrab2  30261  isarchi  30811  bnj1189  32281  dfacycgr1  32391  fmlasucdisj  32646  dfon3  33353  wl-hadnot  34757  poimirlem18  34925  poimirlem21  34928  poimirlem30  34937  poimirlem31  34938  ftc1anclem3  34984  hdmaplem4  38925  mapdh9a  38940  ifpnot23  39864  ifpdfxor  39873  ifpnim1  39883  ifpnim2  39885  dfsucon  39909  ntrneineine1lem  40454  disjrnmpt2  41469  aiotavb  43310  dfatprc  43349  ndmafv2nrn  43441  nfunsnafv2  43444  oddneven  43829