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  1826  2exnaln  1827  sbn  2284  ralnex  3078  rexanali  3108  r2exlem  3149  nelbOLD  3241  dfss6  3998  nss  4073  difdif  4158  indifdi  4313  difab  4329  neq0  4375  ssdif0  4389  difin0ss  4396  sbcnel12g  4437  disjsn  4736  iundif2  5097  iindif2  5100  brsymdif  5225  rexxfr  5434  nssss  5475  reldm0  5952  domtriord  9189  rnelfmlem  23981  dchrfi  27317  noinfbnd1lem4  27789  wwlksnext  29926  dff15  35060  df3nandALT2  36366  wl-3xornot1  37446  poimirlem1  37581  dvasin  37664  lcvbr3  38979  cvrval2  39230  hashnexinj  42085  wopprc  42987  onsucf1olem  43232  sqrtcvallem1  43593  gneispace  44096  iindif2f  45065  aiota0ndef  47012