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  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  2972  ne3anior  3020  rexab  3669  inssdif0  4340  falseral0  4482  dtruALT  5346  dm0rn0  5891  brprcneu  6851  brprcneuALT  6852  soseq  8141  0nelfz1  13511  pmltpc  25358  cofcutr  27839  nbgrnself  29293  rgrx0ndm  29528  clwwlkneq0  29965  nfrgr2v  30208  frgrncvvdeqlem1  30235  cvbr2  32219  bnj1143  34787  fmlan0  35385  brsset  35884  brtxpsd  35889  dffun10  35909  dfint3  35947  brub  35949  wl-nfeqfb  37531  sbcni  38112  brvdif2  38258  dfssr2  38497  lcvbr2  39022  atlrelat1  39321  dfxor5  43763  df3an2  43765  clsk1independent  44042  spr0nelg  47481  341fppr2  47739  9fppr8  47742  pgrpgt2nabl  48358  lmod1zrnlvec  48487  aacllem  49794