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  2286  ralnex  3062  rexanali  3090  r2exlem  3125  dfss6  3923  nss  3998  difdif  4087  indifdi  4246  difab  4262  neq0  4304  ssdif0  4318  difin0ss  4325  sbcnel12g  4366  disjsn  4668  iundif2  5029  iindif2  5032  brsymdif  5157  rexxfr  5361  nssss  5403  reldm0  5877  domtriord  9051  rnelfmlem  23896  dchrfi  27222  noinfbnd1lem4  27694  wwlksnext  29966  dff15  35240  df3nandALT2  36594  regsfromsetind  36669  wl-3xornot1  37681  poimirlem1  37818  dvasin  37901  lcvbr3  39279  cvrval2  39530  hashnexinj  42378  wopprc  43268  onsucf1olem  43508  sqrtcvallem1  43868  gneispace  44371  iindif2f  45400  aiota0ndef  47339  isubgr3stgrlem3  48210