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  1828  2exnaln  1829  sbn  2280  ralnex  3062  rexanali  3091  r2exlem  3129  dfss6  3948  nss  4023  difdif  4110  indifdi  4269  difab  4285  neq0  4327  ssdif0  4341  difin0ss  4348  sbcnel12g  4389  disjsn  4687  iundif2  5050  iindif2  5053  brsymdif  5178  rexxfr  5386  nssss  5430  reldm0  5907  domtriord  9137  rnelfmlem  23890  dchrfi  27218  noinfbnd1lem4  27690  wwlksnext  29875  dff15  35115  df3nandALT2  36418  wl-3xornot1  37498  poimirlem1  37645  dvasin  37728  lcvbr3  39041  cvrval2  39292  hashnexinj  42141  wopprc  43054  onsucf1olem  43294  sqrtcvallem1  43655  gneispace  44158  iindif2f  45184  aiota0ndef  47126  isubgr3stgrlem3  47980