Theorem xchbinxr 338

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

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  con2bii  361  2nalexn  1829  2exnaln  1830  sbn  2283  sbnALT  2571  ralnex  3199  rexanali  3224  nelb  3227  r2exlem  3261  dfss6  3904  nss  3977  difdif  4058  difab  4224  neq0  4259  ssdif0  4277  difin0ss  4282  sbcnel12g  4319  disjsn  4607  iundif2  4959  iindif2  4962  brsymdif  5089  notzfausOLD  5228  rexxfr  5282  nssss  5313  reldm0  5762  domtriord  8647  rnelfmlem  22557  dchrfi  25839  wwlksnext  27679  dff15  32463  df3nandALT2  33861  wl-3xornot1  34897  poimirlem1  35058  dvasin  35141  lcvbr3  36319  cvrval2  36570  wopprc  39971  sqrtcvallem1  40331  gneispace  40837  aiota0ndef  43652