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  2318  necon3abii  3005  ne3anior  3053  rexab  3656  inssdif0OLD  4326  falseral0OLD  4474  dtruALT  5357  dm0rn0OLD  5919  brprcneu  6906  brprcneuALT  6907  soseq  8213  0nelfz1  13716  pmltpc  25826  cofcutr  28367  nbgrnself  29997  rgrx0ndm  30231  clwwlkneq0  30677  nfrgr2v  30930  frgrncvvdeqlem1  30957  cvbr2  32942  bnj1143  35531  fmlan0  36364  brsset  36866  brtxpsd  36871  dffun10  36891  dfint3  36931  brub  36933  regsfromsetind  37542  wl-nfeqfb  38736  sbcni  39309  brvdif2  39465  dfssr2  39777  lcvbr2  40345  atlrelat1  40644  dfxor5  45028  df3an2  45030  clsk1independent  45307  spr0nelg  48831  341fppr2  49105  9fppr8  49108  pgrpgt2nabl  49809  lmod1zrnlvec  49937  aacllem  51367