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  1830  2exnaln  1831  sbn  2287  ralnex  3064  rexanali  3092  r2exlem  3127  dfss6  3912  nss  3987  difdif  4076  indifdi  4235  difab  4251  neq0  4293  ssdif0  4307  difin0ss  4314  sbcnel12g  4355  disjsn  4656  iundif2  5017  iindif2  5020  brsymdif  5145  rexxfr  5353  nssss  5402  reldm0  5877  domtriord  9054  rnelfmlem  23927  dchrfi  27232  noinfbnd1lem4  27704  wwlksnext  29976  dff15  35243  df3nandALT2  36598  regsfromsetind  36737  wl-3xornot1  37810  poimirlem1  37956  dvasin  38039  lcvbr3  39483  cvrval2  39734  hashnexinj  42581  wopprc  43476  onsucf1olem  43716  sqrtcvallem1  44076  gneispace  44579  iindif2f  45608  aiota0ndef  47557  isubgr3stgrlem3  48456