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  3056  rexanali  3085  r2exlem  3123  dfss6  3939  nss  4014  difdif  4101  indifdi  4260  difab  4276  neq0  4318  ssdif0  4332  difin0ss  4339  sbcnel12g  4380  disjsn  4678  iundif2  5041  iindif2  5044  brsymdif  5169  rexxfr  5374  nssss  5418  reldm0  5894  domtriord  9093  rnelfmlem  23846  dchrfi  27173  noinfbnd1lem4  27645  wwlksnext  29830  dff15  35081  df3nandALT2  36395  wl-3xornot1  37475  poimirlem1  37622  dvasin  37705  lcvbr3  39023  cvrval2  39274  hashnexinj  42123  wopprc  43026  onsucf1olem  43266  sqrtcvallem1  43627  gneispace  44130  iindif2f  45161  aiota0ndef  47102  isubgr3stgrlem3  47971