Theorem xchbinxr 334

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 223	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	xchbinx 333	1 ⊢ (𝜑 ↔ ¬ 𝜒)

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  con2bii  357  2nalexn  1830  2exnaln  1831  sbn  2276  ralnex  3072  rexanali  3102  r2exlem  3143  nelbOLD  3232  dfss6  3971  nss  4046  difdif  4130  indifdi  4283  difab  4300  neq0  4345  ssdif0  4363  difin0ss  4368  sbcnel12g  4411  disjsn  4715  iundif2  5077  iindif2  5080  brsymdif  5207  rexxfr  5414  nssss  5455  reldm0  5927  domtriord  9125  rnelfmlem  23463  dchrfi  26765  noinfbnd1lem4  27236  wwlksnext  29185  dff15  34156  df3nandALT2  35371  wl-3xornot1  36447  poimirlem1  36575  dvasin  36658  lcvbr3  37979  cvrval2  38230  wopprc  41851  onsucf1olem  42102  sqrtcvallem1  42464  gneispace  42967  iindif2f  43936  aiota0ndef  45884