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  359  anor  998  pm4.52  1000  pm4.54  1002  xordi  1032  xorcom  1541  xorneg1  1549  xorbi12i  1551  norcom  1557  nornot  1558  noran  1559  trunanfal  1609  truxortru  1612  truxorfal  1613  falxorfal  1615  trunortru  1616  trunorfal  1617  falnorfal  1619  nic-mpALT  1699  nic-axALT  1701  sbex  2322  necon3abii  3010  ne3anior  3058  rexab  3667  inssdif0  4336  falseral0OLD  4478  dtruALT  5357  dm0rn0OLD  5913  brprcneu  6869  brprcneuALT  6870  soseq  8151  0nelfz1  13567  pmltpc  25574  cofcutr  28079  nbgrnself  29646  rgrx0ndm  29880  clwwlkneq0  30317  nfrgr2v  30560  frgrncvvdeqlem1  30587  cvbr2  32572  bnj1143  35119  fmlan0  35778  brsset  36274  brtxpsd  36279  dffun10  36299  dfint3  36339  brub  36341  regsfromsetind  36935  wl-nfeqfb  38074  sbcni  38645  brvdif2  38801  dfssr2  39113  lcvbr2  39681  atlrelat1  39980  dfxor5  44378  df3an2  44380  clsk1independent  44657  spr0nelg  48107  341fppr2  48381  9fppr8  48384  pgrpgt2nabl  49024  lmod1zrnlvec  49152  aacllem  50457