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  3055  rexanali  3084  r2exlem  3122  dfss6  3936  nss  4011  difdif  4098  indifdi  4257  difab  4273  neq0  4315  ssdif0  4329  difin0ss  4336  sbcnel12g  4377  disjsn  4675  iundif2  5038  iindif2  5041  brsymdif  5166  rexxfr  5371  nssss  5415  reldm0  5891  domtriord  9087  rnelfmlem  23839  dchrfi  27166  noinfbnd1lem4  27638  wwlksnext  29823  dff15  35074  df3nandALT2  36388  wl-3xornot1  37468  poimirlem1  37615  dvasin  37698  lcvbr3  39016  cvrval2  39267  hashnexinj  42116  wopprc  43019  onsucf1olem  43259  sqrtcvallem1  43620  gneispace  44123  iindif2f  45154  aiota0ndef  47098  isubgr3stgrlem3  47967