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

Theorem xchbinxr 335
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 223 . 2 (𝜓𝜒)
41, 3xchbinx 334 1 (𝜑 ↔ ¬ 𝜒)
Colors of variables: wff setvar class
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  358  2nalexn  1831  2exnaln  1832  sbn  2277  ralnex  3076  rexanali  3106  r2exlem  3141  nelbOLD  3224  dfss6  3934  nss  4007  difdif  4091  indifdi  4244  difab  4261  neq0  4306  ssdif0  4324  difin0ss  4329  sbcnel12g  4372  disjsn  4673  iundif2  5035  iindif2  5038  brsymdif  5165  rexxfr  5372  nssss  5413  reldm0  5884  domtriord  9068  rnelfmlem  23306  dchrfi  26606  noinfbnd1lem4  27077  wwlksnext  28841  dff15  33691  df3nandALT2  34875  wl-3xornot1  35954  poimirlem1  36082  dvasin  36165  lcvbr3  37488  cvrval2  37739  wopprc  41357  onsucf1olem  41608  sqrtcvallem1  41910  gneispace  42413  iindif2f  43382  aiota0ndef  45336
  Copyright terms: Public domain W3C validator