Theorem xchbinxr 338

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 227	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	xchbinx 337	1 ⊢ (𝜑 ↔ ¬ 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  con2bii  360  nbbn  386  2nalexn  1860  2exnaln  1861  sbn  2313  ralnex  3088  rexanali  3116  r2exlem  3151  dfss6  3898  nss  3972  difdif  4071  indifdi  4239  difab  4255  neq0  4298  ssdif0  4313  difin0ss  4320  sbcnel12g  4371  disjsn  4668  iundif2  5031  iindif2  5036  brsymdif  5158  rexxfr  5377  nssss  5422  reldm0  5909  dff15  7276  domtriord  9145  rnelfmlem  24276  dchrfi  27587  noinfbnd1lem4  28088  wwlksnext  30487  df3nandALT2  37280  regsfromsetind  37419  qdiffALT  38342  wl-3xornot1  38496  poimirlem1  38632  dvasin  38715  lcvbr3  40173  cvrval2  40424  hashnexinj  43271  wopprc  44130  onsucf1olem  44365  sqrtcvallem1  44724  gneispace  45227  iindif2f  46268  aiota0ndef  48260  isubgr3stgrlem3  49159