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 275	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  982  pm4.52  984  pm4.54  986  xordi  1016  xorcom  1513  xorneg1  1522  xorbi12i  1524  norcom  1531  nornot  1533  noran  1534  trunanfal  1584  truxortru  1587  truxorfal  1588  falxorfal  1590  trunortru  1591  trunorfal  1592  falnorfal  1594  nic-mpALT  1675  nic-axALT  1677  sbex  2278  necon3abii  2988  ne3anior  3037  rexab  3690  inssdif0  4369  falseral0  4519  dtruALT  5386  dm0rn0  5923  brprcneu  6879  brprcneuALT  6880  soseq  8142  0nelfz1  13517  pmltpc  24959  cofcutr  27401  nbgrnself  28606  rgrx0ndm  28840  clwwlkneq0  29272  nfrgr2v  29515  frgrncvvdeqlem1  29542  cvbr2  31524  bnj1143  33790  fmlan0  34371  brsset  34850  brtxpsd  34855  dffun10  34875  dfint3  34913  brub  34915  wl-nfeqfb  36394  sbcni  36968  brvdif2  37119  dfssr2  37358  lcvbr2  37881  atlrelat1  38180  dfxor5  42504  df3an2  42506  clsk1independent  42783  spr0nelg  46131  341fppr2  46389  9fppr8  46392  pgrpgt2nabl  46996  lmod1zrnlvec  47129  aacllem  47802