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

Theorem xchbinx 302
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 288 . 2  |-  ( -. 
ps 
<->  -.  ch )
41, 3bitri 241 1  |-  ( ph  <->  -. 
ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177
This theorem is referenced by:  xchbinxr  303  con1bii  322  pm4.52  478  pm4.54  480  xordi  866  3anor  950  nannan  1297  nannot  1299  nanbi  1300  truxortru  1364  truxorfal  1365  falxorfal  1367  nic-mpALT  1443  nic-axALT  1445  sban  2103  sbex  2163  necon3abii  2581  ne3anior  2637  inssdif0  3639  dtruALT  4338  dtruALT2  4350  dm0rn0  5027  brprcneu  5662  pmltpc  19215  cvbr2  23635  soseq  25279  brsset  25454  brtxpsd  25459  frgrancvvdeqlem2  27784  bnj1143  28500  sbanNEW7  28906  sbexNEW7  28951  lcvbr2  29138  atlrelat1  29437
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator