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  2978  ne3anior  3026  rexab  3678  inssdif0  4349  falseral0  4491  dtruALT  5358  dm0rn0  5904  brprcneu  6865  brprcneuALT  6866  soseq  8156  0nelfz1  13558  pmltpc  25401  cofcutr  27875  nbgrnself  29284  rgrx0ndm  29519  clwwlkneq0  29956  nfrgr2v  30199  frgrncvvdeqlem1  30226  cvbr2  32210  bnj1143  34767  fmlan0  35359  brsset  35853  brtxpsd  35858  dffun10  35878  dfint3  35916  brub  35918  wl-nfeqfb  37500  sbcni  38081  brvdif2  38226  dfssr2  38463  lcvbr2  38986  atlrelat1  39285  dfxor5  43738  df3an2  43740  clsk1independent  44017  spr0nelg  47438  341fppr2  47696  9fppr8  47699  pgrpgt2nabl  48289  lmod1zrnlvec  48418  aacllem  49613