Theorem xchbinxr 335

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

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  con2bii  357  2nalexn  1824  2exnaln  1825  sbn  2278  ralnex  3069  rexanali  3099  r2exlem  3140  nelbOLD  3232  dfss6  3984  nss  4059  difdif  4144  indifdi  4299  difab  4315  neq0  4357  ssdif0  4371  difin0ss  4378  sbcnel12g  4419  disjsn  4715  iundif2  5078  iindif2  5081  brsymdif  5206  rexxfr  5421  nssss  5465  reldm0  5940  domtriord  9161  rnelfmlem  23975  dchrfi  27313  noinfbnd1lem4  27785  wwlksnext  29922  dff15  35076  df3nandALT2  36382  wl-3xornot1  37462  poimirlem1  37607  dvasin  37690  lcvbr3  39004  cvrval2  39255  hashnexinj  42109  wopprc  43018  onsucf1olem  43259  sqrtcvallem1  43620  gneispace  44123  iindif2f  45102  aiota0ndef  47046  isubgr3stgrlem3  47870