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  1829  2exnaln  1830  sbn  2275  ralnex  3071  rexanali  3101  r2exlem  3142  nelbOLD  3231  dfss6  3972  nss  4047  difdif  4131  indifdi  4284  difab  4301  neq0  4346  ssdif0  4364  difin0ss  4369  sbcnel12g  4412  disjsn  4716  iundif2  5078  iindif2  5081  brsymdif  5208  rexxfr  5415  nssss  5456  reldm0  5928  domtriord  9126  rnelfmlem  23677  dchrfi  26991  noinfbnd1lem4  27462  wwlksnext  29411  dff15  34382  df3nandALT2  35589  wl-3xornot1  36665  poimirlem1  36793  dvasin  36876  lcvbr3  38197  cvrval2  38448  wopprc  42072  onsucf1olem  42323  sqrtcvallem1  42685  gneispace  43188  iindif2f  44157  aiota0ndef  46105