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  1830  2exnaln  1831  sbn  2287  ralnex  3063  rexanali  3091  r2exlem  3126  dfss6  3911  nss  3986  difdif  4075  indifdi  4234  difab  4250  neq0  4292  ssdif0  4306  difin0ss  4313  sbcnel12g  4354  disjsn  4655  iundif2  5016  iindif2  5019  brsymdif  5144  rexxfr  5358  nssss  5407  reldm0  5883  domtriord  9061  rnelfmlem  23917  dchrfi  27218  noinfbnd1lem4  27690  wwlksnext  29961  dff15  35227  df3nandALT2  36582  regsfromsetind  36721  qdiffALT  37642  wl-3xornot1  37796  poimirlem1  37942  dvasin  38025  lcvbr3  39469  cvrval2  39720  hashnexinj  42567  wopprc  43458  onsucf1olem  43698  sqrtcvallem1  44058  gneispace  44561  iindif2f  45590  aiota0ndef  47545  isubgr3stgrlem3  48444