Theorem xchbinxr 335

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

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  con2bii  357  2nalexn  1828  2exnaln  1829  sbn  2280  ralnex  3055  rexanali  3083  r2exlem  3118  dfss6  3927  nss  4002  difdif  4088  indifdi  4247  difab  4263  neq0  4305  ssdif0  4319  difin0ss  4326  sbcnel12g  4367  disjsn  4665  iundif2  5026  iindif2  5029  brsymdif  5154  rexxfr  5358  nssss  5402  reldm0  5874  domtriord  9047  rnelfmlem  23855  dchrfi  27182  noinfbnd1lem4  27654  wwlksnext  29856  dff15  35050  df3nandALT2  36373  wl-3xornot1  37453  poimirlem1  37600  dvasin  37683  lcvbr3  39001  cvrval2  39252  hashnexinj  42101  wopprc  43003  onsucf1olem  43243  sqrtcvallem1  43604  gneispace  44107  iindif2f  45138  aiota0ndef  47082  isubgr3stgrlem3  47953