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 ⊢ (𝜑 ↔ ¬ 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  xchbinxr  338  con1bii  359  anor  998  pm4.52  1000  pm4.54  1002  xordi  1034  xorcom  1543  xorneg1  1551  xorbi12i  1553  norcom  1559  nornot  1560  noran  1561  trunanfal  1611  truxortru  1614  truxorfal  1615  falxorfal  1617  trunortru  1618  trunorfal  1619  falnorfal  1621  nic-mpALT  1704  nic-axALT  1706  sbex  2314  necon3abii  3001  ne3anior  3049  rexab  3652  inssdif0OLD  4322  falseral0OLD  4470  dtruALT  5349  dm0rn0OLD  5906  brprcneu  6876  brprcneuALT  6877  soseq  8179  0nelfz1  13680  pmltpc  25777  cofcutr  28316  nbgrnself  29946  rgrx0ndm  30180  clwwlkneq0  30626  nfrgr2v  30879  frgrncvvdeqlem1  30906  cvbr2  32891  bnj1143  35467  fmlan0  36243  brsset  36744  brtxpsd  36749  dffun10  36769  dfint3  36809  brub  36811  regsfromsetind  37420  wl-nfeqfb  38562  sbcni  39137  brvdif2  39293  dfssr2  39605  lcvbr2  40173  atlrelat1  40472  dfxor5  44861  df3an2  44863  clsk1independent  45140  spr0nelg  48652  341fppr2  48926  9fppr8  48929  pgrpgt2nabl  49572  lmod1zrnlvec  49700  aacllem  51108