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  1829  2exnaln  1830  sbn  2282  ralnex  3058  rexanali  3086  r2exlem  3121  dfss6  3924  nss  3999  difdif  4085  indifdi  4244  difab  4260  neq0  4302  ssdif0  4316  difin0ss  4323  sbcnel12g  4364  disjsn  4664  iundif2  5022  iindif2  5025  brsymdif  5150  rexxfr  5354  nssss  5396  reldm0  5868  domtriord  9036  rnelfmlem  23865  dchrfi  27191  noinfbnd1lem4  27663  wwlksnext  29869  dff15  35091  df3nandALT2  36433  wl-3xornot1  37513  poimirlem1  37660  dvasin  37743  lcvbr3  39061  cvrval2  39312  hashnexinj  42160  wopprc  43062  onsucf1olem  43302  sqrtcvallem1  43663  gneispace  44166  iindif2f  45196  aiota0ndef  47127  isubgr3stgrlem3  47998