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

Theorem xchbinx 334
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 320 . 2 𝜓 ↔ ¬ 𝜒)
41, 3bitri 275 1 (𝜑 ↔ ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206
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 207
This theorem is referenced by:  xchbinxr  335  con1bii  356  anor  985  pm4.52  987  pm4.54  989  xordi  1019  xorcom  1514  xorneg1  1522  xorbi12i  1524  norcom  1530  nornot  1531  noran  1532  trunanfal  1582  truxortru  1585  truxorfal  1586  falxorfal  1588  trunortru  1589  trunorfal  1590  falnorfal  1592  nic-mpALT  1672  nic-axALT  1674  sbex  2281  necon3abii  2987  ne3anior  3036  rexab  3700  inssdif0  4374  falseral0  4516  dtruALT  5388  dm0rn0  5935  brprcneu  6896  brprcneuALT  6897  soseq  8184  0nelfz1  13583  pmltpc  25485  cofcutr  27958  nbgrnself  29376  rgrx0ndm  29611  clwwlkneq0  30048  nfrgr2v  30291  frgrncvvdeqlem1  30318  cvbr2  32302  bnj1143  34804  fmlan0  35396  brsset  35890  brtxpsd  35895  dffun10  35915  dfint3  35953  brub  35955  wl-nfeqfb  37537  sbcni  38118  brvdif2  38263  dfssr2  38500  lcvbr2  39023  atlrelat1  39322  dfxor5  43780  df3an2  43782  clsk1independent  44059  spr0nelg  47463  341fppr2  47721  9fppr8  47724  pgrpgt2nabl  48282  lmod1zrnlvec  48411  aacllem  49320
  Copyright terms: Public domain W3C validator