Theorem xchbinxr 325

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 324	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:  3anor  1052  2nalexn  1752  2exnaln  1753  sbn  2390  ralnex  2988  ralnexOLD  2989  rexanali  2994  r2exlem  3054  nss  3648  difdif  3720  difab  3878  ssdif0  3922  difin0ss  3926  sbcnel12g  3963  disjsn  4223  iundif2  4560  iindif2  4562  brsymdif  4681  notzfaus  4810  rexxfr  4858  nssss  4895  reldm0  5313  domtriord  8066  rnelfmlem  21696  dchrfi  24914  wwlksnext  26691  df3nandALT2  32092  bj-ssbn  32336  poimirlem1  33081  dvasin  33167  lcvbr3  33829  cvrval2  34080  wopprc  37116  dfss6  37583  gneispace  37953