Theorem xchbinxr 324

Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)

Hypotheses

Ref	Expression
xchbinxr.1	⊢ (𝜑 ↔ ¬ 𝜓)
xchbinxr.2	⊢ (𝜒 ↔ 𝜓)

Assertion

Ref	Expression
xchbinxr	⊢ (𝜑 ↔ ¬ 𝜒)

Proof of Theorem xchbinxr

Step	Hyp	Ref	Expression
1		xchbinxr.1	. 2 ⊢ (𝜑 ↔ ¬ 𝜓)
2		xchbinxr.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	2	bicomi 214	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	xchbinx 323	1 ⊢ (𝜑 ↔ ¬ 𝜒)

Syntax hints:  ¬ wn 3   ↔ wb 196

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 197

This theorem is referenced by:  3anorOLD  1072  2nalexn  1795  2exnaln  1796  sbn  2419  ralnex  3021  ralnexOLD  3022  rexanali  3027  r2exlem  3088  dfss6  3626  nss  3696  difdif  3769  difab  3929  ssdif0  3975  difin0ss  3979  sbcnel12g  4018  disjsn  4278  iundif2  4619  iindif2  4621  brsymdif  4744  notzfaus  4870  rexxfr  4918  nssss  4954  reldm0  5375  domtriord  8147  rnelfmlem  21803  dchrfi  25025  wwlksnext  26856  df3nandALT2  32522  bj-ssbn  32766  poimirlem1  33540  dvasin  33626  lcvbr3  34628  cvrval2  34879  wopprc  37914  gneispace  38749