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  511  pm4.54  513  xordi  955  3anorOLD  1072  nancom  1490  nannot  1493  xorneg1  1515  trunanfal  1565  truxortru  1568  truxorfal  1569  falxorfal  1571  nic-mpALT  1637  nic-axALT  1639  sban  2427  sbex  2491  necon3abii  2869  ne3anior  2916  ralnex2  3074  ralnex3  3075  inssdif0  3980  falseral0  4114  dtruALT  4929  dtruALT2  4941  dm0rn0  5374  brprcneu  6222  0nelfz1  12398  pmltpc  23265  nbgrnself  26300  rgrx0ndm  26545  clwwlkneq0  26990  nfrgr2v  27252  frgrncvvdeqlem1  27279  cvbr2  29270  bnj1143  30987  soseq  31879  brsset  32121  brtxpsd  32126  dffun10  32146  dfint3  32184  brub  32186  wl-nfeqfb  33453  sbcni  34044  brvdif2  34167  dfssr2  34389  lcvbr2  34627  atlrelat1  34926  dfxor5  38376  df3an2  38378  clsk1independent  38661  spr0nelg  42051  pgrpgt2nabl  42472  lmod1zrnlvec  42608  aacllem  42875
 Copyright terms: Public domain W3C validator