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  1515  xorneg1  1523  xorbi12i  1525  norcom  1531  nornot  1532  noran  1533  trunanfal  1583  truxortru  1586  truxorfal  1587  falxorfal  1589  trunortru  1590  trunorfal  1591  falnorfal  1593  nic-mpALT  1673  nic-axALT  1675  sbex  2283  necon3abii  2974  ne3anior  3022  rexab  3649  inssdif0  4319  falseral0  4461  dtruALT  5321  dm0rn0OLD  5860  brprcneu  6807  brprcneuALT  6808  soseq  8084  0nelfz1  13438  pmltpc  25373  cofcutr  27863  nbgrnself  29332  rgrx0ndm  29567  clwwlkneq0  30001  nfrgr2v  30244  frgrncvvdeqlem1  30271  cvbr2  32255  bnj1143  34794  fmlan0  35427  brsset  35923  brtxpsd  35928  dffun10  35948  dfint3  35986  brub  35988  wl-nfeqfb  37570  sbcni  38151  brvdif2  38297  dfssr2  38536  lcvbr2  39061  atlrelat1  39360  dfxor5  43800  df3an2  43802  clsk1independent  44079  spr0nelg  47507  341fppr2  47765  9fppr8  47768  pgrpgt2nabl  48397  lmod1zrnlvec  48526  aacllem  49833