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  2118  sbex  2178  necon3abii  2597  ne3anior  2653  inssdif0  3655  dtruALT  4356  dtruALT2  4368  dm0rn0  5045  brprcneu  5680  pmltpc  19300  cvbr2  23739  soseq  25468  brsset  25643  brtxpsd  25648  frgrancvvdeqlem2  28134  bnj1143  28867  sbanNEW7  29273  sbexNEW7  29318  lcvbr2  29505  atlrelat1  29804
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