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  984  pm4.52  986  pm4.54  988  xordi  1018  xorcom  1515  xorneg1  1523  xorbi12i  1525  norcom  1531  nornot  1532  noran  1533  trunanfal  1583  truxortru  1586  truxorfal  1587  falxorfal  1589  trunortru  1590  trunorfal  1591  falnorfal  1593  nic-mpALT  1673  nic-axALT  1675  sbex  2287  necon3abii  2978  ne3anior  3026  rexab  3653  inssdif0  4326  falseral0OLD  4468  dtruALT  5333  dm0rn0OLD  5874  brprcneu  6824  brprcneuALT  6825  soseq  8101  0nelfz1  13459  pmltpc  25407  cofcutr  27920  nbgrnself  29432  rgrx0ndm  29667  clwwlkneq0  30104  nfrgr2v  30347  frgrncvvdeqlem1  30374  cvbr2  32358  bnj1143  34946  fmlan0  35585  brsset  36081  brtxpsd  36086  dffun10  36106  dfint3  36146  brub  36148  regsfromsetind  36669  wl-nfeqfb  37741  sbcni  38312  brvdif2  38460  dfssr2  38752  lcvbr2  39282  atlrelat1  39581  dfxor5  44008  df3an2  44010  clsk1independent  44287  spr0nelg  47722  341fppr2  47980  9fppr8  47983  pgrpgt2nabl  48612  lmod1zrnlvec  48740  aacllem  50046