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  1861  2exnaln  1862  sbn  2318  ralnex  3094  rexanali  3122  r2exlem  3157  dfss6  3930  nss  4004  difdif  4092  indifdi  4250  difab  4266  neq0  4309  ssdif0  4324  difin0ss  4331  sbcnel12g  4382  disjsn  4682  iundif2  5043  iindif2  5048  brsymdif  5175  rexxfr  5392  nssss  5441  reldm0  5923  dff15  7277  domtriord  9121  rnelfmlem  24146  dchrfi  27456  noinfbnd1lem4  27927  wwlksnext  30279  df3nandALT2  36952  regsfromsetind  37091  qdiffALT  38013  wl-3xornot1  38167  poimirlem1  38313  dvasin  38396  lcvbr3  39838  cvrval2  40089  hashnexinj  42936  wopprc  43798  onsucf1olem  44038  sqrtcvallem1  44398  gneispace  44901  iindif2f  45919  aiota0ndef  47875  isubgr3stgrlem3  48774