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  1510  xorneg1  1518  xorbi12i  1520  norcom  1526  nornot  1527  noran  1528  trunanfal  1578  truxortru  1581  truxorfal  1582  falxorfal  1584  trunortru  1585  trunorfal  1586  falnorfal  1588  nic-mpALT  1668  nic-axALT  1670  sbex  2279  necon3abii  2984  ne3anior  3033  rexab  3702  inssdif0  4379  falseral0  4521  dtruALT  5393  dm0rn0  5937  brprcneu  6896  brprcneuALT  6897  soseq  8182  0nelfz1  13579  pmltpc  25498  cofcutr  27972  nbgrnself  29390  rgrx0ndm  29625  clwwlkneq0  30057  nfrgr2v  30300  frgrncvvdeqlem1  30327  cvbr2  32311  bnj1143  34782  fmlan0  35375  brsset  35870  brtxpsd  35875  dffun10  35895  dfint3  35933  brub  35935  wl-nfeqfb  37516  sbcni  38097  brvdif2  38243  dfssr2  38480  lcvbr2  39003  atlrelat1  39302  dfxor5  43756  df3an2  43758  clsk1independent  44035  spr0nelg  47400  341fppr2  47658  9fppr8  47661  pgrpgt2nabl  48210  lmod1zrnlvec  48339  aacllem  49031