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 274	1 ⊢ (𝜑 ↔ ¬ 𝜒)

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  xchbinxr  335  con1bii  357  anor  980  pm4.52  982  pm4.54  984  xordi  1014  xorcom  1509  xorneg1  1518  xorbi12i  1520  norcom  1527  nornot  1529  noran  1530  trunanfal  1581  truxortru  1584  truxorfal  1585  falxorfal  1587  trunortru  1588  trunorfal  1589  falnorfal  1592  falnorfalOLD  1593  nic-mpALT  1675  nic-axALT  1677  sbex  2279  necon3abii  2991  ne3anior  3039  rexab  3632  inssdif0  4304  falseral0  4451  dtruALT  5312  dm0rn0  5837  brprcneu  6773  brprcneuALT  6774  0nelfz1  13284  pmltpc  24623  nbgrnself  27735  rgrx0ndm  27969  clwwlkneq0  28402  nfrgr2v  28645  frgrncvvdeqlem1  28672  cvbr2  30654  bnj1143  32779  fmlan0  33362  soseq  33812  cofcutr  34101  brsset  34200  brtxpsd  34205  dffun10  34225  dfint3  34263  brub  34265  wl-nfeqfb  35704  sbcni  36278  brvdif2  36409  dfssr2  36624  lcvbr2  37043  atlrelat1  37342  dfxor5  41382  df3an2  41384  clsk1independent  41663  spr0nelg  44939  341fppr2  45197  9fppr8  45200  pgrpgt2nabl  45713  lmod1zrnlvec  45846  aacllem  46516