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  2314  ralnex  3089  rexanali  3117  r2exlem  3152  dfss6  3921  nss  3995  difdif  4082  indifdi  4240  difab  4256  neq0  4299  ssdif0  4314  difin0ss  4321  sbcnel12g  4372  disjsn  4672  iundif2  5032  iindif2  5037  brsymdif  5164  rexxfr  5378  nssss  5423  reldm0  5910  dff15  7268  domtriord  9126  rnelfmlem  24251  dchrfi  27564  noinfbnd1lem4  28065  wwlksnext  30464  df3nandALT2  37158  regsfromsetind  37297  qdiffALT  38217  wl-3xornot1  38371  poimirlem1  38507  dvasin  38590  lcvbr3  40048  cvrval2  40299  hashnexinj  43146  wopprc  43990  onsucf1olem  44230  sqrtcvallem1  44590  gneispace  45093  iindif2f  46118  aiota0ndef  48111  isubgr3stgrlem3  49010