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

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced 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  1702  nic-axALT  1704  sbex  2316  necon3abii  3004  ne3anior  3052  rexab  3659  inssdif0OLD  4331  falseral0OLD  4477  dtruALT  5361  dm0rn0OLD  5917  brprcneu  6873  brprcneuALT  6874  soseq  8156  0nelfz1  13572  pmltpc  25590  cofcutr  28098  nbgrnself  29690  rgrx0ndm  29924  clwwlkneq0  30361  nfrgr2v  30604  frgrncvvdeqlem1  30631  cvbr2  32616  bnj1143  35159  fmlan0  35864  brsset  36360  brtxpsd  36365  dffun10  36385  dfint3  36425  brub  36427  regsfromsetind  37031  wl-nfeqfb  38172  sbcni  38741  brvdif2  38897  dfssr2  39209  lcvbr2  39777  atlrelat1  40076  dfxor5  44476  df3an2  44478  clsk1independent  44755  spr0nelg  48208  341fppr2  48482  9fppr8  48485  pgrpgt2nabl  49129  lmod1zrnlvec  49257  aacllem  50584