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 224 . 2 (𝜓𝜒)
41, 3xchbinx 334 1 (𝜑 ↔ ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206
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 207
This theorem is referenced by:  con2bii  357  2nalexn  1828  2exnaln  1829  sbn  2280  ralnex  3072  rexanali  3102  r2exlem  3143  nelbOLD  3235  dfss6  3973  nss  4048  difdif  4135  indifdi  4294  difab  4310  neq0  4352  ssdif0  4366  difin0ss  4373  sbcnel12g  4414  disjsn  4711  iundif2  5074  iindif2  5077  brsymdif  5202  rexxfr  5416  nssss  5460  reldm0  5938  domtriord  9163  rnelfmlem  23960  dchrfi  27299  noinfbnd1lem4  27771  wwlksnext  29913  dff15  35098  df3nandALT2  36401  wl-3xornot1  37481  poimirlem1  37628  dvasin  37711  lcvbr3  39024  cvrval2  39275  hashnexinj  42129  wopprc  43042  onsucf1olem  43283  sqrtcvallem1  43644  gneispace  44147  iindif2f  45165  aiota0ndef  47109  isubgr3stgrlem3  47935
  Copyright terms: Public domain W3C validator