MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xchbinx Structured version   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  1300  nannot  1302  nanbi  1303  truxortru  1367  truxorfal  1368  falxorfal  1370  nic-mpALT  1446  nic-axALT  1448  sban  2143  sbex  2204  necon3abii  2628  ne3anior  2684  inssdif0  3687  dtruALT  4388  dtruALT2  4400  dm0rn0  5078  brprcneu  5713  pmltpc  19337  cvbr2  23776  soseq  25514  brsset  25699  brtxpsd  25704  dffun10  25724  dfint3  25762  brub  25764  frgrancvvdeqlem2  28321  bnj1143  29062  sbanNEW7  29470  sbexNEW7  29518  lcvbr2  29721  atlrelat1  30020
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