Theorem xchbinx 336

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

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  xchbinxr  337  con1bii  358  anor  995  pm4.52  997  pm4.54  999  xordi  1029  xorcom  1533  xorneg1  1541  xorbi12i  1543  norcom  1549  nornot  1550  noran  1551  trunanfal  1601  truxortru  1604  truxorfal  1605  falxorfal  1607  trunortru  1608  trunorfal  1609  falnorfal  1611  nic-mpALT  1691  nic-axALT  1693  sbex  2314  necon3abii  3002  ne3anior  3050  rexab  3656  inssdif0  4324  falseral0OLD  4466  dtruALT  5342  dm0rn0OLD  5897  brprcneu  6852  brprcneuALT  6853  soseq  8133  0nelfz1  13542  pmltpc  25500  cofcutr  28005  nbgrnself  29517  rgrx0ndm  29751  clwwlkneq0  30188  nfrgr2v  30431  frgrncvvdeqlem1  30458  cvbr2  32443  bnj1143  35046  fmlan0  35702  brsset  36198  brtxpsd  36203  dffun10  36223  dfint3  36263  brub  36265  regsfromsetind  36860  wl-nfeqfb  38000  sbcni  38571  brvdif2  38727  dfssr2  39039  lcvbr2  39607  atlrelat1  39906  dfxor5  44304  df3an2  44306  clsk1independent  44583  spr0nelg  48043  341fppr2  48317  9fppr8  48320  pgrpgt2nabl  48949  lmod1zrnlvec  49077  aacllem  50383