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  1544  xorneg1  1552  xorbi12i  1554  norcom  1560  nornot  1561  noran  1562  trunanfal  1612  truxortru  1615  truxorfal  1616  falxorfal  1618  trunortru  1619  trunorfal  1620  falnorfal  1622  nic-mpALT  1705  nic-axALT  1707  sbex  2315  necon3abii  3002  ne3anior  3050  rexab  3653  inssdif0OLD  4323  falseral0OLD  4471  dtruALT  5350  dm0rn0OLD  5907  brprcneu  6873  brprcneuALT  6874  soseq  8169  0nelfz1  13669  pmltpc  25764  cofcutr  28303  nbgrnself  29933  rgrx0ndm  30167  clwwlkneq0  30613  nfrgr2v  30866  frgrncvvdeqlem1  30893  cvbr2  32878  bnj1143  35413  fmlan0  36135  brsset  36631  brtxpsd  36636  dffun10  36656  dfint3  36696  brub  36698  regsfromsetind  37307  wl-nfeqfb  38448  sbcni  39023  brvdif2  39179  dfssr2  39491  lcvbr2  40059  atlrelat1  40358  dfxor5  44752  df3an2  44754  clsk1independent  45031  spr0nelg  48527  341fppr2  48801  9fppr8  48804  pgrpgt2nabl  49447  lmod1zrnlvec  49575  aacllem  50908