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 206

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 207

This theorem is referenced by:  xchbinxr  335  con1bii  356  anor  985  pm4.52  987  pm4.54  989  xordi  1019  xorcom  1516  xorneg1  1524  xorbi12i  1526  norcom  1532  nornot  1533  noran  1534  trunanfal  1584  truxortru  1587  truxorfal  1588  falxorfal  1590  trunortru  1591  trunorfal  1592  falnorfal  1594  nic-mpALT  1674  nic-axALT  1676  sbex  2288  necon3abii  2979  ne3anior  3027  rexab  3642  inssdif0  4315  falseral0OLD  4456  dtruALT  5325  dm0rn0OLD  5874  brprcneu  6824  brprcneuALT  6825  soseq  8102  0nelfz1  13488  pmltpc  25427  cofcutr  27930  nbgrnself  29442  rgrx0ndm  29677  clwwlkneq0  30114  nfrgr2v  30357  frgrncvvdeqlem1  30384  cvbr2  32369  bnj1143  34948  fmlan0  35589  brsset  36085  brtxpsd  36090  dffun10  36110  dfint3  36150  brub  36152  regsfromsetind  36737  wl-nfeqfb  37875  sbcni  38446  brvdif2  38602  dfssr2  38914  lcvbr2  39482  atlrelat1  39781  dfxor5  44212  df3an2  44214  clsk1independent  44491  spr0nelg  47948  341fppr2  48222  9fppr8  48225  pgrpgt2nabl  48854  lmod1zrnlvec  48982  aacllem  50288