Theorem xchbinx 337

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 323	. 2 ⊢ (¬ 𝜓 ↔ ¬ 𝜒)
4	1, 3	bitri 278	1 ⊢ (𝜑 ↔ ¬ 𝜒)

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  xchbinxr  338  con1bii  360  anor  980  pm4.52  982  pm4.54  984  xordi  1014  xorcom  1505  xorneg1  1514  xorbi12i  1516  norcom  1523  nornot  1525  noran  1527  trunanfal  1580  truxortru  1583  truxorfal  1584  falxorfal  1586  trunortru  1587  trunorfal  1589  falnorfal  1592  falnorfalOLD  1593  nic-mpALT  1674  nic-axALT  1676  sbex  2284  sbanOLD  2308  sbanvOLD  2319  sbanALT  2586  necon3abii  3033  ne3anior  3080  inssdif0  4283  falseral0  4417  dtruALT  5254  dtruALT2  5301  dm0rn0  5759  brprcneu  6637  0nelfz1  12921  pmltpc  24054  nbgrnself  27149  rgrx0ndm  27383  clwwlkneq0  27814  nfrgr2v  28057  frgrncvvdeqlem1  28084  cvbr2  30066  bnj1143  32172  fmlan0  32751  soseq  33209  brsset  33463  brtxpsd  33468  dffun10  33488  dfint3  33526  brub  33528  wl-nfeqfb  34941  wl-dfrexsb  35016  sbcni  35549  brvdif2  35683  dfssr2  35899  lcvbr2  36318  atlrelat1  36617  dfxor5  40468  df3an2  40470  clsk1independent  40749  spr0nelg  43993  341fppr2  44252  9fppr8  44255  pgrpgt2nabl  44768  lmod1zrnlvec  44903  aacllem  45329