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  4236  undif3  4267  2nreu  4395  intirr  5980  ordtri3or  6225  nf1const  7061  nf1oconst  7062  frxp  7822  ressuppssdif  7853  suppofssd  7869  domunfican  8793  ssfin4  9734  prinfzo0  13079  swrdnnn0nd  14020  swrdnd0  14021  lcmfunsnlem2lem1  15984  ncoprmlnprm  16070  prm23ge5  16154  smndex2dnrinv  18082  symgfix2  18546  gsumdixp  19361  cnfldfunALT  20560  symgmatr01lem  21264  ppttop  21617  zclmncvs  23754  mdegleb  24660  2lgslem3  25982  trlsegvdeg  28008  strlem1  30029  difrab2  30263  isarchi  30813  bnj1189  32283  dfacycgr1  32393  fmlasucdisj  32648  dfon3  33355  poimirlem18  34912  poimirlem21  34915  poimirlem30  34924  poimirlem31  34925  ftc1anclem3  34971  hdmaplem4  38912  mapdh9a  38927  ifpnot23  39851  ifpdfxor  39860  ifpnim1  39870  ifpnim2  39872  dfsucon  39896  ntrneineine1lem  40441  disjrnmpt2  41456  aiotavb  43297  dfatprc  43336  ndmafv2nrn  43428  nfunsnafv2  43431  oddneven  43816