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  nbbn  385  2nalexn  1847  2exnaln  1848  sbn  2313  ralnex  3087  rexanali  3115  r2exlem  3150  dfss6  3926  nss  4000  difdif  4088  indifdi  4246  difab  4262  neq0  4304  ssdif0  4318  difin0ss  4325  sbcnel12g  4367  disjsn  4669  iundif2  5030  iindif2  5033  brsymdif  5158  rexxfr  5372  nssss  5421  reldm0  5902  domtriord  9091  rnelfmlem  23992  dchrfi  27296  noinfbnd1lem4  27767  wwlksnext  30039  dff15  35342  df3nandALT2  36724  regsfromsetind  36863  qdiffALT  37784  wl-3xornot1  37938  poimirlem1  38084  dvasin  38167  lcvbr3  39611  cvrval2  39862  hashnexinj  42709  wopprc  43571  onsucf1olem  43811  sqrtcvallem1  44171  gneispace  44674  iindif2f  45702  aiota0ndef  47655  isubgr3stgrlem3  48554