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

Theorem xchbinx 311
Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
Hypotheses
Ref Expression
xchbinx.1  |-  ( ph  <->  -. 
ps )
xchbinx.2  |-  ( ps  <->  ch )
Assertion
Ref Expression
xchbinx  |-  ( ph  <->  -. 
ch )

Proof of Theorem xchbinx
StepHypRef Expression
1 xchbinx.1 . 2  |-  ( ph  <->  -. 
ps )
2 xchbinx.2 . . 3  |-  ( ps  <->  ch )
32notbii 297 . 2  |-  ( -. 
ps 
<->  -.  ch )
41, 3bitri 252 1  |-  ( ph  <->  -. 
ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187
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 188
This theorem is referenced by:  xchbinxr  312  con1bii  332  pm4.52  493  pm4.54  495  xordi  903  3anor  998  nancom  1382  nannanOLD  1385  nannot  1387  nanbiOLDOLD  1390  xorneg1  1412  trunanfal  1482  truxortru  1486  truxorfal  1487  falxorfal  1490  nic-mpALT  1551  nic-axALT  1553  sban  2191  sbex  2256  necon3abii  2682  ne3anior  2748  ralnex2  2929  ralnex3  2930  inssdif0  3859  dtruALT  4645  dtruALT2  4657  dm0rn0  5062  brprcneu  5865  0nelfz1  11805  pmltpc  22308  frgrancvvdeqlem2  25645  cvbr2  27812  bnj1143  29431  soseq  30320  brsset  30482  brtxpsd  30487  dffun10  30507  dfint3  30545  brub  30547  wl-nfeqfb  31618  sbcni  32097  lcvbr2  32341  atlrelat1  32640  dfxor5  36046  pgrpgt2nabl  38968  lmod1zrnlvec  39104  aacllem  39358
  Copyright terms: Public domain W3C validator