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  1516  xorneg1  1524  xorbi12i  1526  norcom  1532  nornot  1533  noran  1534  trunanfal  1584  truxortru  1587  truxorfal  1588  falxorfal  1590  trunortru  1591  trunorfal  1592  falnorfal  1594  nic-mpALT  1674  nic-axALT  1676  sbex  2288  necon3abii  2978  ne3anior  3026  rexab  3641  inssdif0  4314  falseral0OLD  4455  dtruALT  5330  dm0rn0OLD  5880  brprcneu  6830  brprcneuALT  6831  soseq  8109  0nelfz1  13497  pmltpc  25417  cofcutr  27916  nbgrnself  29428  rgrx0ndm  29662  clwwlkneq0  30099  nfrgr2v  30342  frgrncvvdeqlem1  30369  cvbr2  32354  bnj1143  34932  fmlan0  35573  brsset  36069  brtxpsd  36074  dffun10  36094  dfint3  36134  brub  36136  regsfromsetind  36721  wl-nfeqfb  37861  sbcni  38432  brvdif2  38588  dfssr2  38900  lcvbr2  39468  atlrelat1  39767  dfxor5  44194  df3an2  44196  clsk1independent  44473  spr0nelg  47936  341fppr2  48210  9fppr8  48213  pgrpgt2nabl  48842  lmod1zrnlvec  48970  aacllem  50276