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

Theorem xchbinx 336
Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
Hypotheses
Ref Expression
xchbinx.1 (𝜑 ↔ ¬ 𝜓)
xchbinx.2 (𝜓𝜒)
Assertion
Ref Expression
xchbinx (𝜑 ↔ ¬ 𝜒)

Proof of Theorem xchbinx
StepHypRef Expression
1 xchbinx.1 . 2 (𝜑 ↔ ¬ 𝜓)
2 xchbinx.2 . . 3 (𝜓𝜒)
32notbii 322 . 2 𝜓 ↔ ¬ 𝜒)
41, 3bitri 277 1 (𝜑 ↔ ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 208
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 209
This theorem is referenced by:  xchbinxr  337  con1bii  359  anor  978  pm4.52  980  pm4.54  982  xordi  1012  xorneg1  1508  nornot  1517  noran  1519  trunanfal  1572  truxortru  1575  truxorfal  1576  falxorfal  1578  trunortru  1579  trunorfal  1581  falnorfal  1584  falnorfalOLD  1585  nic-mpALT  1666  nic-axALT  1668  sbex  2281  sbanOLD  2305  sbanvOLD  2319  sbanALT  2604  necon3abii  3060  ne3anior  3108  ralnex2OLD  3259  ralnex3OLD  3261  inssdif0  4327  falseral0  4457  dtruALT  5279  dtruALT2  5326  dm0rn0  5788  brprcneu  6655  0nelfz1  12918  pmltpc  24043  nbgrnself  27133  rgrx0ndm  27367  clwwlkneq0  27799  nfrgr2v  28043  frgrncvvdeqlem1  28070  cvbr2  30052  bnj1143  32050  fmlan0  32626  soseq  33084  brsset  33338  brtxpsd  33343  dffun10  33363  dfint3  33401  brub  33403  wl-nfeqfb  34758  wl-dfrexsb  34833  sbcni  35371  brvdif2  35505  dfssr2  35721  lcvbr2  36140  atlrelat1  36439  dfxor5  40092  df3an2  40094  clsk1independent  40376  spr0nelg  43618  341fppr2  43879  9fppr8  43882  pgrpgt2nabl  44394  lmod1zrnlvec  44529  aacllem  44882
  Copyright terms: Public domain W3C validator