Theorem xchbinx 337

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  xchbinxr  338  con1bii  359  anor  998  pm4.52  1000  pm4.54  1002  xordi  1034  xorcom  1544  xorneg1  1552  xorbi12i  1554  norcom  1560  nornot  1561  noran  1562  trunanfal  1612  truxortru  1615  truxorfal  1616  falxorfal  1618  trunortru  1619  trunorfal  1620  falnorfal  1622  nic-mpALT  1705  nic-axALT  1707  sbex  2318  necon3abii  3006  ne3anior  3054  rexab  3660  inssdif0OLD  4330  falseral0OLD  4478  dtruALT  5361  dm0rn0OLD  5917  brprcneu  6875  brprcneuALT  6876  soseq  8157  0nelfz1  13582  pmltpc  25638  cofcutr  28146  nbgrnself  29738  rgrx0ndm  29972  clwwlkneq0  30409  nfrgr2v  30652  frgrncvvdeqlem1  30679  cvbr2  32664  bnj1143  35202  fmlan0  35896  brsset  36392  brtxpsd  36397  dffun10  36417  dfint3  36457  brub  36459  regsfromsetind  37083  wl-nfeqfb  38224  sbcni  38793  brvdif2  38949  dfssr2  39261  lcvbr2  39829  atlrelat1  40128  dfxor5  44526  df3an2  44528  clsk1independent  44805  spr0nelg  48258  341fppr2  48532  9fppr8  48535  pgrpgt2nabl  49179  lmod1zrnlvec  49307  aacllem  50654