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  2314  necon3abii  3001  ne3anior  3049  rexab  3653  inssdif0OLD  4323  falseral0OLD  4471  dtruALT  5353  dm0rn0OLD  5909  brprcneu  6868  brprcneuALT  6869  soseq  8157  0nelfz1  13597  pmltpc  25678  cofcutr  28189  nbgrnself  29819  rgrx0ndm  30053  clwwlkneq0  30499  nfrgr2v  30752  frgrncvvdeqlem1  30779  cvbr2  32764  bnj1143  35299  fmlan0  35970  brsset  36466  brtxpsd  36471  dffun10  36491  dfint3  36531  brub  36533  regsfromsetind  37158  wl-nfeqfb  38299  sbcni  38859  brvdif2  39015  dfssr2  39327  lcvbr2  39895  atlrelat1  40194  dfxor5  44607  df3an2  44609  clsk1independent  44886  spr0nelg  48376  341fppr2  48650  9fppr8  48653  pgrpgt2nabl  49296  lmod1zrnlvec  49424  aacllem  50772