MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xchbinxr Structured version   Visualization version   GIF version

Theorem xchbinxr 324
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
StepHypRef Expression
1 xchbinxr.1 . 2 (𝜑 ↔ ¬ 𝜓)
2 xchbinxr.2 . . 3 (𝜒𝜓)
32bicomi 214 . 2 (𝜓𝜒)
41, 3xchbinx 323 1 (𝜑 ↔ ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196
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 197
This theorem is referenced by:  3anorOLD  1072  2nalexn  1795  2exnaln  1796  sbn  2419  ralnex  3021  ralnexOLD  3022  rexanali  3027  r2exlem  3088  dfss6  3626  nss  3696  difdif  3769  difab  3929  ssdif0  3975  difin0ss  3979  sbcnel12g  4018  disjsn  4278  iundif2  4619  iindif2  4621  brsymdif  4744  notzfaus  4870  rexxfr  4918  nssss  4954  reldm0  5375  domtriord  8147  rnelfmlem  21803  dchrfi  25025  wwlksnext  26856  df3nandALT2  32522  bj-ssbn  32766  poimirlem1  33540  dvasin  33626  lcvbr3  34628  cvrval2  34879  wopprc  37914  gneispace  38749
  Copyright terms: Public domain W3C validator