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  1515  xorneg1  1523  xorbi12i  1525  norcom  1531  nornot  1532  noran  1533  trunanfal  1583  truxortru  1586  truxorfal  1587  falxorfal  1589  trunortru  1590  trunorfal  1591  falnorfal  1593  nic-mpALT  1673  nic-axALT  1675  sbex  2285  necon3abii  2975  ne3anior  3023  rexab  3650  inssdif0  4323  falseral0OLD  4465  dtruALT  5330  dm0rn0OLD  5871  brprcneu  6821  brprcneuALT  6822  soseq  8098  0nelfz1  13450  pmltpc  25398  cofcutr  27888  nbgrnself  29358  rgrx0ndm  29593  clwwlkneq0  30030  nfrgr2v  30273  frgrncvvdeqlem1  30300  cvbr2  32284  bnj1143  34874  fmlan0  35507  brsset  36003  brtxpsd  36008  dffun10  36028  dfint3  36068  brub  36070  wl-nfeqfb  37653  sbcni  38224  brvdif2  38372  dfssr2  38664  lcvbr2  39194  atlrelat1  39493  dfxor5  43924  df3an2  43926  clsk1independent  44203  spr0nelg  47638  341fppr2  47896  9fppr8  47899  pgrpgt2nabl  48528  lmod1zrnlvec  48656  aacllem  49962