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

Theorem xchbinxr 325
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 324 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:  3anor  1052  2nalexn  1752  2exnaln  1753  sbn  2390  ralnex  2988  ralnexOLD  2989  rexanali  2994  r2exlem  3054  nss  3648  difdif  3720  difab  3878  ssdif0  3922  difin0ss  3926  sbcnel12g  3963  disjsn  4223  iundif2  4560  iindif2  4562  brsymdif  4681  notzfaus  4810  rexxfr  4858  nssss  4895  reldm0  5313  domtriord  8066  rnelfmlem  21696  dchrfi  24914  wwlksnext  26691  df3nandALT2  32092  bj-ssbn  32336  poimirlem1  33081  dvasin  33167  lcvbr3  33829  cvrval2  34080  wopprc  37116  dfss6  37583  gneispace  37953
  Copyright terms: Public domain W3C validator