Theorem xchbinx 333

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 319	. 2 ⊢ (¬ 𝜓 ↔ ¬ 𝜒)
4	1, 3	bitri 274	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:  xchbinxr  334  con1bii  355  anor  980  pm4.52  982  pm4.54  984  xordi  1014  xorcom  1507  xorneg1  1515  xorbi12i  1517  norcom  1523  nornot  1524  noran  1525  trunanfal  1575  truxortru  1578  truxorfal  1579  falxorfal  1581  trunortru  1582  trunorfal  1583  falnorfal  1585  nic-mpALT  1666  nic-axALT  1668  sbex  2270  necon3abii  2976  ne3anior  3025  rexab  3686  inssdif0  4371  falseral0  4521  dtruALT  5388  dm0rn0  5927  brprcneu  6886  brprcneuALT  6887  soseq  8164  0nelfz1  13555  pmltpc  25423  cofcutr  27890  nbgrnself  29244  rgrx0ndm  29479  clwwlkneq0  29911  nfrgr2v  30154  frgrncvvdeqlem1  30181  cvbr2  32165  bnj1143  34549  fmlan0  35129  brsset  35613  brtxpsd  35618  dffun10  35638  dfint3  35676  brub  35678  wl-nfeqfb  37131  sbcni  37712  brvdif2  37861  dfssr2  38098  lcvbr2  38621  atlrelat1  38920  dfxor5  43336  df3an2  43338  clsk1independent  43615  spr0nelg  46950  341fppr2  47208  9fppr8  47211  pgrpgt2nabl  47613  lmod1zrnlvec  47745  aacllem  48417