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 ⊢ (𝜑 ↔ ¬ 𝜒)

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  con2bii  360  nbbn  386  2nalexn  1858  2exnaln  1859  sbn  2315  ralnex  3091  rexanali  3119  r2exlem  3154  dfss6  3928  nss  4002  difdif  4090  indifdi  4248  difab  4264  neq0  4307  ssdif0  4322  difin0ss  4329  sbcnel12g  4380  disjsn  4678  iundif2  5039  iindif2  5044  brsymdif  5171  rexxfr  5389  nssss  5438  reldm0  5920  domtriord  9112  rnelfmlem  24090  dchrfi  27397  noinfbnd1lem4  27868  wwlksnext  30220  dff15  35450  df3nandALT2  36889  regsfromsetind  37028  qdiffALT  37950  wl-3xornot1  38104  poimirlem1  38250  dvasin  38333  lcvbr3  39775  cvrval2  40026  hashnexinj  42873  wopprc  43737  onsucf1olem  43977  sqrtcvallem1  44337  gneispace  44840  iindif2f  45858  aiota0ndef  47811  isubgr3stgrlem3  48710