Theorem xchbinxr 327

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

Syntax hints:  ¬ wn 3   ↔ wb 198

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 199

This theorem is referenced by:  2nalexn  1871  2exnaln  1872  sbn  2467  ralnex  3174  rexanali  3179  r2exlem  3244  dfss6  3811  nss  3882  difdif  3959  difab  4122  ssdif0  4172  difin0ss  4177  sbcnel12g  4210  disjsn  4478  iundif2  4822  iindif2  4824  brsymdif  4947  notzfaus  5076  rexxfr  5130  nssss  5158  reldm0  5590  domtriord  8396  rnelfmlem  22175  dchrfi  25443  wwlksnext  27271  df3nandALT2  32991  bj-ssbn  33239  poimirlem1  34045  dvasin  34130  lcvbr3  35186  cvrval2  35437  wopprc  38570  gneispace  39402  aiota0ndef  42139