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

Theorem xchbinx 323
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 309 . 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  324  con1bii  345  pm4.52  969  pm4.54  971  xordi  1002  3anorOLD  1094  nancom  1598  nannot  1601  xorneg1  1623  trunanfal  1673  truxortru  1676  truxorfal  1677  falxorfal  1679  nic-mpALT  1745  nic-axALT  1747  sban  2546  sbex  2611  necon3abii  2989  ne3anior  3036  ralnex2  3193  ralnex3  3194  inssdif0  4094  falseral0  4220  dtruALT  5027  dtruALT2  5039  dm0rn0  5480  brprcneu  6325  0nelfz1  12567  pmltpc  23438  nbgrnself  26478  rgrx0ndm  26724  clwwlkneq0  27183  nfrgr2v  27454  frgrncvvdeqlem1  27481  cvbr2  29482  bnj1143  31199  soseq  32091  brsset  32333  brtxpsd  32338  dffun10  32358  dfint3  32396  brub  32398  wl-nfeqfb  33658  sbcni  34246  brvdif2  34369  dfssr2  34591  lcvbr2  34831  atlrelat1  35130  dfxor5  38585  df3an2  38587  clsk1independent  38870  spr0nelg  42254  pgrpgt2nabl  42675  lmod1zrnlvec  42811  aacllem  43078
  Copyright terms: Public domain W3C validator