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  359  2nalexn  1836  2exnaln  1837  sbn  2293  ralnex  3067  rexanali  3095  r2exlem  3130  dfss6  3907  nss  3981  difdif  4068  indifdi  4225  difab  4241  neq0  4283  ssdif0  4297  difin0ss  4304  sbcnel12g  4345  disjsn  4646  iundif2  5006  iindif2  5009  brsymdif  5134  rexxfr  5348  nssss  5397  reldm0  5877  domtriord  9055  rnelfmlem  23939  dchrfi  27240  noinfbnd1lem4  27712  wwlksnext  29983  dff15  35280  df3nandALT2  36643  regsfromsetind  36782  qdiffALT  37703  wl-3xornot1  37857  poimirlem1  38003  dvasin  38086  lcvbr3  39530  cvrval2  39781  hashnexinj  42628  wopprc  43490  onsucf1olem  43730  sqrtcvallem1  44090  gneispace  44593  iindif2f  45621  aiota0ndef  47574  isubgr3stgrlem3  48473