Theorem xchbinx 323

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 309	. 2 ⊢ (¬ 𝜓 ↔ ¬ 𝜒)
4	1, 3	bitri 264	1 ⊢ (𝜑 ↔ ¬ 𝜒)

Syntax hints:  ¬ wn 3   ↔ wb 196

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 197

This theorem is referenced by:  xchbinxr  324  con1bii  345  pm4.52  969  pm4.54  971  xordi  1002  3anorOLD  1094  nancom  1598  nannot  1601  xorneg1  1623  trunanfal  1673  truxortru  1676  truxorfal  1677  falxorfal  1679  nic-mpALT  1745  nic-axALT  1747  sban  2546  sbex  2611  necon3abii  2989  ne3anior  3036  ralnex2  3193  ralnex3  3194  inssdif0  4094  falseral0  4220  dtruALT  5027  dtruALT2  5039  dm0rn0  5480  brprcneu  6325  0nelfz1  12567  pmltpc  23438  nbgrnself  26478  rgrx0ndm  26724  clwwlkneq0  27183  nfrgr2v  27454  frgrncvvdeqlem1  27481  cvbr2  29482  bnj1143  31199  soseq  32091  brsset  32333  brtxpsd  32338  dffun10  32358  dfint3  32396  brub  32398  wl-nfeqfb  33658  sbcni  34246  brvdif2  34369  dfssr2  34591  lcvbr2  34831  atlrelat1  35130  dfxor5  38585  df3an2  38587  clsk1independent  38870  spr0nelg  42254  pgrpgt2nabl  42675  lmod1zrnlvec  42811  aacllem  43078