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 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  335  con1bii  356  anor  980  pm4.52  982  pm4.54  984  xordi  1014  xorcom  1511  xorneg1  1520  xorbi12i  1522  norcom  1529  nornot  1531  noran  1532  trunanfal  1582  truxortru  1585  truxorfal  1586  falxorfal  1588  trunortru  1589  trunorfal  1590  falnorfal  1592  nic-mpALT  1673  nic-axALT  1675  sbex  2276  necon3abii  2986  ne3anior  3035  rexab  3690  inssdif0  4369  falseral0  4519  dtruALT  5386  dm0rn0  5924  brprcneu  6881  brprcneuALT  6882  soseq  8150  0nelfz1  13527  pmltpc  25299  cofcutr  27758  nbgrnself  29050  rgrx0ndm  29284  clwwlkneq0  29716  nfrgr2v  29959  frgrncvvdeqlem1  29986  cvbr2  31970  bnj1143  34266  fmlan0  34847  brsset  35332  brtxpsd  35337  dffun10  35357  dfint3  35395  brub  35397  wl-nfeqfb  36871  sbcni  37445  brvdif2  37596  dfssr2  37835  lcvbr2  38358  atlrelat1  38657  dfxor5  42983  df3an2  42985  clsk1independent  43262  spr0nelg  46605  341fppr2  46863  9fppr8  46866  pgrpgt2nabl  47207  lmod1zrnlvec  47339  aacllem  48012