Theorem xchbinxr 325

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

Syntax hints:  ¬ wn 3   ↔ wb 196

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 197

This theorem is referenced by:  3anor  1054  2nalexn  1755  2exnaln  1756  sbn  2391  ralnex  2992  ralnexOLD  2993  rexanali  2998  r2exlem  3059  dfss6  3593  nss  3663  difdif  3736  difab  3896  ssdif0  3942  difin0ss  3946  sbcnel12g  3985  disjsn  4246  iundif2  4587  iindif2  4589  brsymdif  4711  notzfaus  4840  rexxfr  4888  nssss  4924  reldm0  5343  domtriord  8106  rnelfmlem  21756  dchrfi  24980  wwlksnext  26788  df3nandALT2  32397  bj-ssbn  32641  poimirlem1  33410  dvasin  33496  lcvbr3  34310  cvrval2  34561  wopprc  37597  gneispace  38432