Theorem xchbinxr 336

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 225	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	xchbinx 335	1 ⊢ (𝜑 ↔ ¬ 𝜒)

Syntax hints:  ¬ wn 3   ↔ wb 207

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 208

This theorem is referenced by:  con2bii  358  2nalexn  1835  2exnaln  1836  sbn  2291  ralnex  3066  rexanali  3094  r2exlem  3129  dfss6  3912  nss  3986  difdif  4072  indifdi  4229  difab  4245  neq0  4287  ssdif0  4301  difin0ss  4308  sbcnel12g  4349  disjsn  4650  iundif2  5010  iindif2  5013  brsymdif  5138  rexxfr  5352  nssss  5401  reldm0  5877  domtriord  9058  rnelfmlem  23942  dchrfi  27243  noinfbnd1lem4  27715  wwlksnext  29986  dff15  35272  df3nandALT2  36635  regsfromsetind  36774  qdiffALT  37695  wl-3xornot1  37849  poimirlem1  37995  dvasin  38078  lcvbr3  39522  cvrval2  39773  hashnexinj  42620  wopprc  43482  onsucf1olem  43722  sqrtcvallem1  44082  gneispace  44585  iindif2f  45614  aiota0ndef  47567  isubgr3stgrlem3  48466