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

Syntax hints:  ¬ wn 3   ↔ wb 195

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 196

This theorem is referenced by:  3anor  1047  2nalexn  1745  2exnaln  1746  sbn  2379  ralnex  2975  ralnexOLD  2976  rexanali  2981  r2exlem  3041  nss  3626  difdif  3698  difab  3855  ssdif0  3896  difin0ss  3900  sbcnel12g  3937  disjsn  4192  iundif2  4523  iindif2  4525  brsymdif  4641  notzfaus  4766  rexxfr  4814  nssss  4851  reldm0  5264  domtriord  7991  rnelfmlem  21566  dchrfi  24780  wwlknext  26252  df3nandALT2  31567  bj-ssbn  31830  poimirlem1  32580  dvasin  32666  lcvbr3  33328  cvrval2  33579  wopprc  36615  dfss6  37082  gneispace  37452  wwlksnext  41099