Theorem xchbinxr 324

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 323	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:  3anorOLD  1094  2nalexn  1892  2exnaln  1893  sbn  2516  ralnex  3118  ralnexOLD  3119  rexanali  3124  r2exlem  3185  dfss6  3722  nss  3792  difdif  3867  difab  4027  ssdif0  4073  difin0ss  4077  sbcnel12g  4116  disjsn  4378  iundif2  4727  iindif2  4729  brsymdif  4851  notzfaus  4977  rexxfr  5025  nssss  5061  reldm0  5486  domtriord  8259  rnelfmlem  21928  dchrfi  25150  wwlksnext  26982  df3nandALT2  32674  bj-ssbn  32918  poimirlem1  33692  dvasin  33778  lcvbr3  34782  cvrval2  35033  wopprc  38068  gneispace  38903