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  983  pm4.52  985  pm4.54  987  xordi  1017  xorcom  1511  xorneg1  1519  xorbi12i  1521  norcom  1527  nornot  1528  noran  1529  trunanfal  1579  truxortru  1582  truxorfal  1583  falxorfal  1585  trunortru  1586  trunorfal  1587  falnorfal  1589  nic-mpALT  1670  nic-axALT  1672  sbex  2285  necon3abii  2993  ne3anior  3042  rexab  3716  inssdif0  4397  falseral0  4539  dtruALT  5406  dm0rn0  5949  brprcneu  6910  brprcneuALT  6911  soseq  8200  0nelfz1  13603  pmltpc  25504  cofcutr  27976  nbgrnself  29394  rgrx0ndm  29629  clwwlkneq0  30061  nfrgr2v  30304  frgrncvvdeqlem1  30331  cvbr2  32315  bnj1143  34766  fmlan0  35359  brsset  35853  brtxpsd  35858  dffun10  35878  dfint3  35916  brub  35918  wl-nfeqfb  37490  sbcni  38071  brvdif2  38218  dfssr2  38455  lcvbr2  38978  atlrelat1  39277  dfxor5  43729  df3an2  43731  clsk1independent  44008  spr0nelg  47350  341fppr2  47608  9fppr8  47611  pgrpgt2nabl  48091  lmod1zrnlvec  48223  aacllem  48895