Theorem xchbinx 334

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 320	. 2 ⊢ (¬ 𝜓 ↔ ¬ 𝜒)
4	1, 3	bitri 275	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:  xchbinxr  335  con1bii  356  anor  984  pm4.52  986  pm4.54  988  xordi  1018  xorcom  1514  xorneg1  1522  xorbi12i  1524  norcom  1530  nornot  1531  noran  1532  trunanfal  1582  truxortru  1585  truxorfal  1586  falxorfal  1588  trunortru  1589  trunorfal  1590  falnorfal  1592  nic-mpALT  1672  nic-axALT  1674  sbex  2281  necon3abii  2971  ne3anior  3019  rexab  3663  inssdif0  4333  falseral0  4475  dtruALT  5338  dm0rn0  5878  brprcneu  6830  brprcneuALT  6831  soseq  8115  0nelfz1  13480  pmltpc  25327  cofcutr  27808  nbgrnself  29262  rgrx0ndm  29497  clwwlkneq0  29931  nfrgr2v  30174  frgrncvvdeqlem1  30201  cvbr2  32185  bnj1143  34753  fmlan0  35351  brsset  35850  brtxpsd  35855  dffun10  35875  dfint3  35913  brub  35915  wl-nfeqfb  37497  sbcni  38078  brvdif2  38224  dfssr2  38463  lcvbr2  38988  atlrelat1  39287  dfxor5  43729  df3an2  43731  clsk1independent  44008  spr0nelg  47450  341fppr2  47708  9fppr8  47711  pgrpgt2nabl  48327  lmod1zrnlvec  48456  aacllem  49763