Theorem xchbinx 334

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

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  xchbinxr  335  con1bii  356  anor  985  pm4.52  987  pm4.54  989  xordi  1019  xorcom  1514  xorneg1  1522  xorbi12i  1524  norcom  1530  nornot  1531  noran  1532  trunanfal  1582  truxortru  1585  truxorfal  1586  falxorfal  1588  trunortru  1589  trunorfal  1590  falnorfal  1592  nic-mpALT  1672  nic-axALT  1674  sbex  2281  necon3abii  2987  ne3anior  3036  rexab  3700  inssdif0  4374  falseral0  4516  dtruALT  5388  dm0rn0  5935  brprcneu  6896  brprcneuALT  6897  soseq  8184  0nelfz1  13583  pmltpc  25485  cofcutr  27958  nbgrnself  29376  rgrx0ndm  29611  clwwlkneq0  30048  nfrgr2v  30291  frgrncvvdeqlem1  30318  cvbr2  32302  bnj1143  34804  fmlan0  35396  brsset  35890  brtxpsd  35895  dffun10  35915  dfint3  35953  brub  35955  wl-nfeqfb  37537  sbcni  38118  brvdif2  38263  dfssr2  38500  lcvbr2  39023  atlrelat1  39322  dfxor5  43780  df3an2  43782  clsk1independent  44059  spr0nelg  47463  341fppr2  47721  9fppr8  47724  pgrpgt2nabl  48282  lmod1zrnlvec  48411  aacllem  49320