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  4337  falseral0OLD  4481  dtruALT  5360  dm0rn0OLD  5916  brprcneu  6872  brprcneuALT  6873  soseq  8155  0nelfz1  13571  pmltpc  25578  cofcutr  28083  nbgrnself  29650  rgrx0ndm  29884  clwwlkneq0  30321  nfrgr2v  30564  frgrncvvdeqlem1  30591  cvbr2  32576  bnj1143  35123  fmlan0  35816  brsset  36312  brtxpsd  36317  dffun10  36337  dfint3  36377  brub  36379  regsfromsetind  36973  wl-nfeqfb  38113  sbcni  38684  brvdif2  38840  dfssr2  39152  lcvbr2  39720  atlrelat1  40019  dfxor5  44419  df3an2  44421  clsk1independent  44698  spr0nelg  48148  341fppr2  48422  9fppr8  48425  pgrpgt2nabl  49065  lmod1zrnlvec  49193  aacllem  50509