Theorem xchbinxr 337

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

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  con2bii  360  2nalexn  1824  2exnaln  1825  sbn  2283  sbnOLD  2537  sbnALT  2591  ralnex  3236  rexanali  3265  nelb  3268  r2exlem  3302  dfss6  3956  nss  4028  difdif  4106  difab  4271  ssdif0  4322  difin0ss  4327  sbcnel12g  4362  disjsn  4640  iundif2  4988  iindif2  4991  brsymdif  5117  notzfausOLD  5255  rexxfr  5308  nssss  5340  reldm0  5792  domtriord  8657  rnelfmlem  22554  dchrfi  25825  wwlksnext  27665  dff15  32348  df3nandALT2  33743  poimirlem1  34887  dvasin  34972  lcvbr3  36153  cvrval2  36404  wopprc  39620  gneispace  40477  aiota0ndef  43289