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  359  anor  979  pm4.52  981  pm4.54  983  xordi  1013  xorcom  1504  xorneg1  1513  xorbi12i  1515  norcom  1522  nornot  1524  noran  1526  trunanfal  1579  truxortru  1582  truxorfal  1583  falxorfal  1585  trunortru  1586  trunorfal  1588  falnorfal  1591  falnorfalOLD  1592  nic-mpALT  1673  nic-axALT  1675  sbex  2288  sbanOLD  2312  sbanvOLD  2326  sbanALT  2610  necon3abii  3064  ne3anior  3112  ralnex2OLD  3263  ralnex3OLD  3265  inssdif0  4331  falseral0  4461  dtruALT  5291  dtruALT2  5338  dm0rn0  5797  brprcneu  6664  0nelfz1  12929  pmltpc  24053  nbgrnself  27143  rgrx0ndm  27377  clwwlkneq0  27809  nfrgr2v  28053  frgrncvvdeqlem1  28080  cvbr2  30062  bnj1143  32064  fmlan0  32640  soseq  33098  brsset  33352  brtxpsd  33357  dffun10  33377  dfint3  33415  brub  33417  wl-nfeqfb  34778  wl-dfrexsb  34853  sbcni  35391  brvdif2  35525  dfssr2  35741  lcvbr2  36160  atlrelat1  36459  dfxor5  40119  df3an2  40121  clsk1independent  40403  spr0nelg  43645  341fppr2  43906  9fppr8  43909  pgrpgt2nabl  44421  lmod1zrnlvec  44556  aacllem  44909