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

Theorem xchbinx 319
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 305 . 2 𝜓 ↔ ¬ 𝜒)
41, 3bitri 259 1 (𝜑 ↔ ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 191
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 192
This theorem is referenced by:  xchbinxr  320  con1bii  340  pm4.52  505  pm4.54  507  xordi  925  3anor  1037  nancom  1431  nannot  1434  xorneg1  1458  trunanfal  1511  truxortru  1515  truxorfal  1516  falxorfal  1519  nic-mpALT  1585  nic-axALT  1587  sban  2282  sbex  2346  necon3abii  2723  ne3anior  2770  ralnex2  2920  ralnex3  2921  inssdif0  3781  dtruALT  4673  dtruALT2  4685  dm0rn0  5100  brprcneu  5920  0nelfz1  11914  pmltpc  22560  frgrancvvdeqlem2  25919  cvbr2  28099  bnj1143  29754  soseq  30643  brsset  30807  brtxpsd  30812  dffun10  30832  dfint3  30870  brub  30872  wl-nfeqfb  32101  sbcni  32585  lcvbr2  32828  atlrelat1  33127  dfxor5  36598  df3an2  36600  falseral0  39508  nbgrnself  39983  rgrx0ndm  40193  nfrgr2v  40842  frgrncvvdeqlem2  40870  pgrpgt2nabl  41341  lmod1zrnlvec  41477  aacllem  41727
  Copyright terms: Public domain W3C validator