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  2291  sbex  2355  necon3abii  2732  ne3anior  2779  ralnex2  2931  ralnex3  2932  inssdif0  3804  dtruALT  4725  dtruALT2  4737  dm0rn0  5154  brprcneu  5985  0nelfz1  12103  pmltpc  22905  frgrancvvdeqlem2  26300  cvbr2  28318  bnj1143  29964  soseq  30841  brsset  31005  brtxpsd  31010  dffun10  31030  dfint3  31068  brub  31070  wl-nfeqfb  32396  sbcni  32978  lcvbr2  33221  atlrelat1  33520  dfxor5  36979  df3an2  36981  clsk1independent  37265  falseral0  40220  nbgrnself  40692  rgrx0ndm  40902  nfrgr2v  41551  frgrncvvdeqlem2  41579  pgrpgt2nabl  42050  lmod1zrnlvec  42186  aacllem  42426
  Copyright terms: Public domain W3C validator