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  3666  inssdif0  4337  falseral0  4479  dtruALT  5343  dm0rn0  5888  brprcneu  6848  brprcneuALT  6849  soseq  8138  0nelfz1  13504  pmltpc  25351  cofcutr  27832  nbgrnself  29286  rgrx0ndm  29521  clwwlkneq0  29958  nfrgr2v  30201  frgrncvvdeqlem1  30228  cvbr2  32212  bnj1143  34780  fmlan0  35378  brsset  35877  brtxpsd  35882  dffun10  35902  dfint3  35940  brub  35942  wl-nfeqfb  37524  sbcni  38105  brvdif2  38251  dfssr2  38490  lcvbr2  39015  atlrelat1  39314  dfxor5  43756  df3an2  43758  clsk1independent  44035  spr0nelg  47477  341fppr2  47735  9fppr8  47738  pgrpgt2nabl  48354  lmod1zrnlvec  48483  aacllem  49790