MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xchbinx Structured version   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  |-  ( 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 296 . 2  |-  ( -. 
ps 
<->  -.  ch )
41, 3bitri 249 1  |-  ( ph  <->  -. 
ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184
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
This theorem is referenced by:  xchbinxr  311  con1bii  331  pm4.52  491  pm4.54  493  xordi  893  3anor  988  nancom  1345  nannanOLD  1348  nannot  1350  nanbiOLD  1352  truxortru  1427  truxorfal  1428  falxorfal  1430  nic-mpALT  1490  nic-axALT  1492  sban  2124  sbex  2191  necon3abii  2701  ne3anior  2767  inssdif0  3877  dtruALT  4665  dtruALT2  4677  dm0rn0  5205  brprcneu  5845  pmltpc  21728  frgrancvvdeqlem2  24896  cvbr2  27067  soseq  29302  brsset  29507  brtxpsd  29512  dffun10  29532  dfint3  29570  brub  29572  wl-nfeqfb  29958  sbcni  30482  ralnex2  31385  pgrpgt2nabl  32667  lmod1zrnlvec  32805  bnj1143  33556  lcvbr2  34449  atlrelat1  34748
  Copyright terms: Public domain W3C validator