Theorem xchbinx 333

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 319	. 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  334  con1bii  356  anor  979  pm4.52  981  pm4.54  983  xordi  1013  xorcom  1506  xorneg1  1515  xorbi12i  1517  norcom  1524  nornot  1526  noran  1528  trunanfal  1581  truxortru  1584  truxorfal  1585  falxorfal  1587  trunortru  1588  trunorfal  1590  falnorfal  1593  falnorfalOLD  1594  nic-mpALT  1676  nic-axALT  1678  sbex  2281  necon3abii  2989  ne3anior  3037  rexab  3624  inssdif0  4300  falseral0  4447  dtruALT  5306  dtruALT2  5353  dm0rn0  5823  brprcneu  6747  fvprc  6748  0nelfz1  13204  pmltpc  24519  nbgrnself  27629  rgrx0ndm  27863  clwwlkneq0  28294  nfrgr2v  28537  frgrncvvdeqlem1  28564  cvbr2  30546  bnj1143  32670  fmlan0  33253  soseq  33730  cofcutr  34019  brsset  34118  brtxpsd  34123  dffun10  34143  dfint3  34181  brub  34183  wl-nfeqfb  35622  sbcni  36196  brvdif2  36328  dfssr2  36544  lcvbr2  36963  atlrelat1  37262  dfxor5  41264  df3an2  41266  clsk1independent  41545  spr0nelg  44816  341fppr2  45074  9fppr8  45077  pgrpgt2nabl  45590  lmod1zrnlvec  45723  aacllem  46391