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  3072  rexanali  3102  r2exlem  3143  nelbOLD  3235  dfss6  3973  nss  4048  difdif  4135  indifdi  4294  difab  4310  neq0  4352  ssdif0  4366  difin0ss  4373  sbcnel12g  4414  disjsn  4711  iundif2  5074  iindif2  5077  brsymdif  5202  rexxfr  5416  nssss  5460  reldm0  5938  domtriord  9163  rnelfmlem  23960  dchrfi  27299  noinfbnd1lem4  27771  wwlksnext  29913  dff15  35098  df3nandALT2  36401  wl-3xornot1  37481  poimirlem1  37628  dvasin  37711  lcvbr3  39024  cvrval2  39275  hashnexinj  42129  wopprc  43042  onsucf1olem  43283  sqrtcvallem1  43644  gneispace  44147  iindif2f  45165  aiota0ndef  47109  isubgr3stgrlem3  47935