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  2317  ralnex  3092  rexanali  3120  r2exlem  3155  dfss6  3903  nss  3977  difdif  4074  indifdi  4242  difab  4258  neq0  4302  ssdif0  4317  difin0ss  4324  sbcnel12g  4375  disjsn  4672  iundif2  5035  iindif2  5040  brsymdif  5162  rexxfr  5382  nssss  5427  reldm0  5917  dff15  7299  domtriord  9170  rnelfmlem  24301  dchrfi  27612  noinfbnd1lem4  28113  wwlksnext  30512  df3nandALT2  37366  regsfromsetind  37505  qdiffALT  38441  wl-3xornot1  38595  poimirlem1  38731  dvasin  38814  lcvbr3  40272  cvrval2  40523  hashnexinj  43370  wopprc  44230  onsucf1olem  44464  sqrtcvallem1  44823  gneispace  45326  iindif2f  46380  aiota0ndef  48372  isubgr3stgrlem3  49271