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  1829  2exnaln  1830  sbn  2284  ralnex  3059  rexanali  3087  r2exlem  3122  dfss6  3920  nss  3995  difdif  4084  indifdi  4243  difab  4259  neq0  4301  ssdif0  4315  difin0ss  4322  sbcnel12g  4363  disjsn  4663  iundif2  5024  iindif2  5027  brsymdif  5152  rexxfr  5356  nssss  5398  reldm0  5872  domtriord  9043  rnelfmlem  23868  dchrfi  27194  noinfbnd1lem4  27666  wwlksnext  29873  dff15  35117  df3nandALT2  36465  wl-3xornot1  37545  poimirlem1  37681  dvasin  37764  lcvbr3  39142  cvrval2  39393  hashnexinj  42241  wopprc  43147  onsucf1olem  43387  sqrtcvallem1  43748  gneispace  44251  iindif2f  45281  aiota0ndef  47221  isubgr3stgrlem3  48092