Theorem xchbinxr 334

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 223	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	xchbinx 333	1 ⊢ (𝜑 ↔ ¬ 𝜒)

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  con2bii  357  2nalexn  1831  2exnaln  1832  sbn  2280  ralnex  3163  rexanali  3191  nelbOLD  3195  r2exlem  3230  dfss6  3906  nss  3979  difdif  4061  indifdi  4214  difab  4231  neq0  4276  ssdif0  4294  difin0ss  4299  sbcnel12g  4342  disjsn  4644  iundif2  4999  iindif2  5002  brsymdif  5129  rexxfr  5334  nssss  5365  reldm0  5826  domtriord  8859  rnelfmlem  23011  dchrfi  26308  wwlksnext  28159  dff15  32956  noinfbnd1lem4  33856  df3nandALT2  34516  wl-3xornot1  35578  poimirlem1  35705  dvasin  35788  lcvbr3  36964  cvrval2  37215  wopprc  40768  sqrtcvallem1  41128  gneispace  41633  aiota0ndef  44476