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

Theorem xchbinx 310
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 296 . 2
41, 3bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184
This theorem is referenced by:  xchbinxr  311  con1bii  331  pm4.52  491  pm4.54  493  xordi  895  3anor  989  nancom  1346  nannanOLD  1349  nannot  1351  nanbiOLD  1353  truxortru  1441  truxorfal  1442  falxorfal  1444  nic-mpALT  1505  nic-axALT  1507  sban  2140  sbex  2207  necon3abii  2717  ne3anior  2783  inssdif0  3895  dtruALT  4684  dtruALT2  4696  dm0rn0  5224  brprcneu  5864  pmltpc  21862  frgrancvvdeqlem2  25031  cvbr2  27202  soseq  29334  brsset  29539  brtxpsd  29544  dffun10  29564  dfint3  29602  brub  29604  wl-nfeqfb  29990  sbcni  30514  ralnex2  31435  pgrpgt2nabl  32959  lmod1zrnlvec  33095  aacllem  33216  bnj1143  33849  lcvbr2  34747  atlrelat1  35046  dfxor5  37790
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 185
  Copyright terms: Public domain W3C validator