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 263 1 (𝜑 ↔ ¬ 𝜒)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195 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 196 This theorem is referenced by:  xchbinxr  324  con1bii  345  pm4.52  511  pm4.54  513  xordi  935  3anor  1047  nancom  1442  nannot  1445  xorneg1  1467  trunanfal  1516  truxortru  1519  truxorfal  1520  falxorfal  1522  nic-mpALT  1588  nic-axALT  1590  sban  2387  sbex  2451  necon3abii  2828  ne3anior  2875  ralnex2  3027  ralnex3  3028  inssdif0  3901  dtruALT  4826  dtruALT2  4838  dm0rn0  5263  brprcneu  6096  0nelfz1  12231  pmltpc  23026  frgrancvvdeqlem2  26558  cvbr2  28526  bnj1143  30115  soseq  30995  brsset  31166  brtxpsd  31171  dffun10  31191  dfint3  31229  brub  31231  wl-nfeqfb  32502  sbcni  33084  lcvbr2  33327  atlrelat1  33626  dfxor5  37078  df3an2  37080  clsk1independent  37364  falseral0  40308  nbgrnself  40583  rgrx0ndm  40793  nfrgr2v  41442  frgrncvvdeqlem2  41470  pgrpgt2nabl  41941  lmod1zrnlvec  42077  aacllem  42356
 Copyright terms: Public domain W3C validator