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  1447  nannot  1450  xorneg1  1472  trunanfal  1522  truxortru  1525  truxorfal  1526  falxorfal  1528  nic-mpALT  1594  nic-axALT  1596  sban  2403  sbex  2467  necon3abii  2842  ne3anior  2889  ralnex2  3043  ralnex3  3044  inssdif0  3926  falseral0  4058  dtruALT  4865  dtruALT2  4877  dm0rn0  5306  brprcneu  6143  0nelfz1  12299  pmltpc  23121  nbgrnself  26138  rgrx0ndm  26353  nfrgr2v  26994  frgrncvvdeqlem2  27022  cvbr2  28982  bnj1143  30561  soseq  31440  brsset  31611  brtxpsd  31616  dffun10  31636  dfint3  31674  brub  31676  wl-nfeqfb  32931  sbcni  33513  lcvbr2  33756  atlrelat1  34055  dfxor5  37507  df3an2  37509  clsk1independent  37793  spr0nelg  40983  pgrpgt2nabl  41390  lmod1zrnlvec  41526  aacllem  41805
  Copyright terms: Public domain W3C validator