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 ⊢ (𝜑 ↔ ¬ 𝜒)

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  con2bii  360  nbbn  386  2nalexn  1851  2exnaln  1852  sbn  2317  ralnex  3091  rexanali  3119  r2exlem  3154  dfss6  3929  nss  4003  difdif  4091  indifdi  4249  difab  4265  neq0  4307  ssdif0  4322  difin0ss  4329  sbcnel12g  4371  disjsn  4673  iundif2  5034  iindif2  5039  brsymdif  5164  rexxfr  5378  nssss  5427  reldm0  5909  domtriord  9099  rnelfmlem  24070  dchrfi  27377  noinfbnd1lem4  27848  wwlksnext  30151  dff15  35388  df3nandALT2  36773  regsfromsetind  36912  qdiffALT  37832  wl-3xornot1  37986  poimirlem1  38132  dvasin  38215  lcvbr3  39659  cvrval2  39910  hashnexinj  42757  wopprc  43619  onsucf1olem  43859  sqrtcvallem1  44219  gneispace  44722  iindif2f  45736  aiota0ndef  47689  isubgr3stgrlem3  48588