Theorem xchbinxr 323

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

Syntax hints:  ¬ wn 3   ↔ wb 194

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 195

This theorem is referenced by:  3anor  1046  2nalexn  1744  2exnaln  1745  sbn  2378  ralnex  2974  ralnexOLD  2975  rexanali  2980  r2exlem  3040  nss  3625  difdif  3697  difab  3854  ssdif0  3895  difin0ss  3899  sbcnel12g  3936  disjsn  4191  iundif2  4517  iindif2  4519  brsymdif  4635  notzfaus  4761  rexxfr  4809  nssss  4845  reldm0  5251  domtriord  7968  rnelfmlem  21508  dchrfi  24697  wwlknext  26018  df3nandALT2  31373  bj-ssbn  31636  poimirlem1  32376  dvasin  32462  lcvbr3  33124  cvrval2  33375  wopprc  36411  dfss6  36878  gneispace  37248  wwlksnext  41094