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  356  2nalexn  1822  2exnaln  1823  sbn  2269  ralnex  3069  rexanali  3099  r2exlem  3140  nelbOLD  3230  dfss6  3971  nss  4046  difdif  4131  indifdi  4286  difab  4303  neq0  4349  ssdif0  4367  difin0ss  4372  sbcnel12g  4415  disjsn  4720  iundif2  5081  iindif2  5084  brsymdif  5211  rexxfr  5420  nssss  5461  reldm0  5934  domtriord  9154  rnelfmlem  23876  dchrfi  27208  noinfbnd1lem4  27679  wwlksnext  29724  dff15  34740  df3nandALT2  35917  wl-3xornot1  36992  poimirlem1  37127  dvasin  37210  lcvbr3  38527  cvrval2  38778  hashnexinj  41631  wopprc  42482  onsucf1olem  42730  sqrtcvallem1  43092  gneispace  43595  iindif2f  44561  aiota0ndef  46506