Theorem xchbinx 323

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 309	. 2 ⊢ (¬ 𝜓 ↔ ¬ 𝜒)
4	1, 3	bitri 263	1 ⊢ (𝜑 ↔ ¬ 𝜒)

Syntax hints:  ¬ wn 3   ↔ wb 195

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 196

This theorem is referenced by:  xchbinxr  324  con1bii  345  pm4.52  511  pm4.54  513  xordi  935  3anor  1047  nancom  1442  nannot  1445  xorneg1  1467  trunanfal  1516  truxortru  1519  truxorfal  1520  falxorfal  1522  nic-mpALT  1588  nic-axALT  1590  sban  2387  sbex  2451  necon3abii  2828  ne3anior  2875  ralnex2  3027  ralnex3  3028  inssdif0  3901  dtruALT  4826  dtruALT2  4838  dm0rn0  5263  brprcneu  6096  0nelfz1  12231  pmltpc  23026  frgrancvvdeqlem2  26558  cvbr2  28526  bnj1143  30115  soseq  30995  brsset  31166  brtxpsd  31171  dffun10  31191  dfint3  31229  brub  31231  wl-nfeqfb  32502  sbcni  33084  lcvbr2  33327  atlrelat1  33626  dfxor5  37078  df3an2  37080  clsk1independent  37364  falseral0  40308  nbgrnself  40583  rgrx0ndm  40793  nfrgr2v  41442  frgrncvvdeqlem2  41470  pgrpgt2nabl  41941  lmod1zrnlvec  42077  aacllem  42356