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  2315  ralnex  3090  rexanali  3118  r2exlem  3153  dfss6  3924  nss  3998  difdif  4085  indifdi  4243  difab  4259  neq0  4302  ssdif0  4317  difin0ss  4324  sbcnel12g  4375  disjsn  4675  iundif2  5036  iindif2  5041  brsymdif  5168  rexxfr  5385  nssss  5434  reldm0  5916  dff15  7273  domtriord  9125  rnelfmlem  24184  dchrfi  27499  noinfbnd1lem4  27970  wwlksnext  30369  df3nandALT2  37027  regsfromsetind  37166  qdiffALT  38088  wl-3xornot1  38242  poimirlem1  38378  dvasin  38461  lcvbr3  39904  cvrval2  40155  hashnexinj  43002  wopprc  43879  onsucf1olem  44119  sqrtcvallem1  44479  gneispace  44982  iindif2f  46000  aiota0ndef  47993  isubgr3stgrlem3  48892