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  985  pm4.52  987  pm4.54  989  xordi  1019  xorcom  1516  xorneg1  1524  xorbi12i  1526  norcom  1532  nornot  1533  noran  1534  trunanfal  1584  truxortru  1587  truxorfal  1588  falxorfal  1590  trunortru  1591  trunorfal  1592  falnorfal  1594  nic-mpALT  1674  nic-axALT  1676  sbex  2288  necon3abii  2979  ne3anior  3027  rexab  3655  inssdif0  4328  falseral0OLD  4470  dtruALT  5335  dm0rn0OLD  5882  brprcneu  6832  brprcneuALT  6833  soseq  8111  0nelfz1  13471  pmltpc  25419  cofcutr  27932  nbgrnself  29444  rgrx0ndm  29679  clwwlkneq0  30116  nfrgr2v  30359  frgrncvvdeqlem1  30386  cvbr2  32370  bnj1143  34965  fmlan0  35604  brsset  36100  brtxpsd  36105  dffun10  36125  dfint3  36165  brub  36167  regsfromsetind  36688  wl-nfeqfb  37788  sbcni  38359  brvdif2  38515  dfssr2  38827  lcvbr2  39395  atlrelat1  39694  dfxor5  44120  df3an2  44122  clsk1independent  44399  spr0nelg  47833  341fppr2  48091  9fppr8  48094  pgrpgt2nabl  48723  lmod1zrnlvec  48851  aacllem  50157