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

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  con2bii  358  2nalexn  1830  2exnaln  1831  sbn  2277  ralnex  3167  rexanali  3192  nelbOLD  3196  r2exlem  3231  dfss6  3910  nss  3983  difdif  4065  indifdi  4217  difab  4234  neq0  4279  ssdif0  4297  difin0ss  4302  sbcnel12g  4345  disjsn  4647  iundif2  5003  iindif2  5006  brsymdif  5133  rexxfr  5339  nssss  5371  reldm0  5837  domtriord  8910  rnelfmlem  23103  dchrfi  26403  wwlksnext  28258  dff15  33056  noinfbnd1lem4  33929  df3nandALT2  34589  wl-3xornot1  35651  poimirlem1  35778  dvasin  35861  lcvbr3  37037  cvrval2  37288  wopprc  40852  sqrtcvallem1  41239  gneispace  41744  aiota0ndef  44589