Theorem xchbinx 326

Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)

Hypotheses

Ref	Expression
xchbinx.1	⊢ (𝜑 ↔ ¬ 𝜓)
xchbinx.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
xchbinx	⊢ (𝜑 ↔ ¬ 𝜒)

Proof of Theorem xchbinx

Step	Hyp	Ref	Expression
1		xchbinx.1	. 2 ⊢ (𝜑 ↔ ¬ 𝜓)
2		xchbinx.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	2	notbii 312	. 2 ⊢ (¬ 𝜓 ↔ ¬ 𝜒)
4	1, 3	bitri 267	1 ⊢ (𝜑 ↔ ¬ 𝜒)

Syntax hints:  ¬ wn 3   ↔ wb 198

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 199

This theorem is referenced by:  xchbinxr  327  con1bii  348  pm4.52  1014  pm4.54  1016  xordi  1047  3anorOLD  1136  nancomOLD  1620  nannotOLD  1625  xorneg1  1650  trunanfal  1701  truxortru  1704  truxorfal  1705  falxorfal  1707  nic-mpALT  1773  nic-axALT  1775  sbanv  2340  sban  2530  sbex  2597  necon3abii  3045  ne3anior  3092  ralnex2  3255  ralnex3  3256  inssdif0  4177  falseral0  4301  dtruALT  5087  dtruALT2  5132  dm0rn0  5574  brprcneu  6425  0nelfz1  12653  pmltpc  23616  nbgrnself  26656  rgrx0ndm  26891  clwwlkneq0  27371  nfrgr2v  27653  frgrncvvdeqlem1  27680  cvbr2  29697  bnj1143  31407  soseq  32293  brsset  32535  brtxpsd  32540  dffun10  32560  dfint3  32598  brub  32600  wl-nfeqfb  33867  sbcni  34455  brvdif2  34580  dfssr2  34797  lcvbr2  35097  atlrelat1  35396  dfxor5  38900  df3an2  38902  clsk1independent  39184  spr0nelg  42573  pgrpgt2nabl  42994  lmod1zrnlvec  43130  aacllem  43443