Theorem xchbinx 335

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

Syntax hints:  ¬ wn 3   ↔ wb 207

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 208

This theorem is referenced by:  xchbinxr  336  con1bii  357  anor  990  pm4.52  992  pm4.54  994  xordi  1024  xorcom  1521  xorneg1  1529  xorbi12i  1531  norcom  1537  nornot  1538  noran  1539  trunanfal  1589  truxortru  1592  truxorfal  1593  falxorfal  1595  trunortru  1596  trunorfal  1597  falnorfal  1599  nic-mpALT  1679  nic-axALT  1681  sbex  2292  necon3abii  2980  ne3anior  3028  rexab  3636  inssdif0  4302  falseral0OLD  4443  dtruALT  5317  dm0rn0OLD  5867  brprcneu  6817  brprcneuALT  6818  soseq  8099  0nelfz1  13488  pmltpc  25435  cofcutr  27934  nbgrnself  29446  rgrx0ndm  29680  clwwlkneq0  30117  nfrgr2v  30360  frgrncvvdeqlem1  30387  cvbr2  32372  bnj1143  34972  fmlan0  35619  brsset  36115  brtxpsd  36120  dffun10  36140  dfint3  36180  brub  36182  regsfromsetind  36767  wl-nfeqfb  37907  sbcni  38478  brvdif2  38634  dfssr2  38946  lcvbr2  39514  atlrelat1  39813  dfxor5  44211  df3an2  44213  clsk1independent  44490  spr0nelg  47951  341fppr2  48225  9fppr8  48228  pgrpgt2nabl  48857  lmod1zrnlvec  48985  aacllem  50291