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  3925  nss  4000  difdif  4089  indifdi  4248  difab  4264  neq0  4306  ssdif0  4320  difin0ss  4327  sbcnel12g  4368  disjsn  4670  iundif2  5031  iindif2  5034  brsymdif  5159  rexxfr  5363  nssss  5410  reldm0  5885  domtriord  9063  rnelfmlem  23908  dchrfi  27234  noinfbnd1lem4  27706  wwlksnext  29978  dff15  35259  df3nandALT2  36613  regsfromsetind  36688  wl-3xornot1  37729  poimirlem1  37866  dvasin  37949  lcvbr3  39393  cvrval2  39644  hashnexinj  42492  wopprc  43381  onsucf1olem  43621  sqrtcvallem1  43981  gneispace  44484  iindif2f  45513  aiota0ndef  47451  isubgr3stgrlem3  48322