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

Theorem xchbinx 324
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 310 . 2 𝜓 ↔ ¬ 𝜒)
41, 3bitri 264 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:  xchbinxr  325  con1bii  346  pm4.52  512  pm4.54  514  xordi  936  3anor  1052  nancom  1448  nannot  1451  xorneg1  1473  trunanfal  1523  truxortru  1526  truxorfal  1527  falxorfal  1529  nic-mpALT  1595  nic-axALT  1597  sban  2397  sbex  2461  necon3abii  2837  ne3anior  2884  ralnex2  3041  ralnex3  3042  inssdif0  3938  falseral0  4072  dtruALT  4890  dtruALT2  4902  dm0rn0  5331  brprcneu  6171  0nelfz1  12345  pmltpc  23200  nbgrnself  26238  rgrx0ndm  26470  nfrgr2v  27116  frgrncvvdeqlem1  27143  cvbr2  29112  bnj1143  30835  soseq  31725  brsset  31971  brtxpsd  31976  dffun10  31996  dfint3  32034  brub  32036  wl-nfeqfb  33294  sbcni  33885  lcvbr2  34128  atlrelat1  34427  dfxor5  37878  df3an2  37880  clsk1independent  38164  spr0nelg  41491  pgrpgt2nabl  41912  lmod1zrnlvec  42048  aacllem  42312
  Copyright terms: Public domain W3C validator