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

Theorem xchbinx 322
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 308 . 2 𝜓 ↔ ¬ 𝜒)
41, 3bitri 262 1 (𝜑 ↔ ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194
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 195
This theorem is referenced by:  xchbinxr  323  con1bii  344  pm4.52  510  pm4.54  512  xordi  934  3anor  1046  nancom  1441  nannot  1444  xorneg1  1466  trunanfal  1515  truxortru  1518  truxorfal  1519  falxorfal  1521  nic-mpALT  1587  nic-axALT  1589  sban  2385  sbex  2449  necon3abii  2826  ne3anior  2873  ralnex2  3025  ralnex3  3026  inssdif0  3899  dtruALT  4820  dtruALT2  4832  dm0rn0  5249  brprcneu  6080  0nelfz1  12185  pmltpc  22942  frgrancvvdeqlem2  26323  cvbr2  28331  bnj1143  29920  soseq  30800  brsset  30971  brtxpsd  30976  dffun10  30996  dfint3  31034  brub  31036  wl-nfeqfb  32304  sbcni  32886  lcvbr2  33129  atlrelat1  33428  dfxor5  36880  df3an2  36882  clsk1independent  37166  falseral0  40112  nbgrnself  40584  rgrx0ndm  40794  nfrgr2v  41443  frgrncvvdeqlem2  41471  pgrpgt2nabl  41942  lmod1zrnlvec  42078  aacllem  42318
  Copyright terms: Public domain W3C validator