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

Theorem xchbinx 303
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 289 . 2  |-  ( -. 
ps 
<->  -.  ch )
41, 3bitri 242 1  |-  ( ph  <->  -. 
ch )
Colors of variables: wff set class
Syntax hints:   -. wn 5    <-> wb 178
This theorem is referenced by:  xchbinxr  304  con1bii  323  pm4.52  479  pm4.54  481  xordi  870  3anor  953  nannan  1296  nannot  1298  nanbi  1299  truxortru  1354  truxorfal  1355  falxorfal  1357  nic-mpALT  1432  nic-axALT  1434  sban  1962  sbex  2091  necon3abii  2449  ne3anior  2505  inssdif0  3482  dtruALT  4165  dtruALT2  4177  dm0rn0  4869  pmltpc  18758  cvbr2  22809  soseq  23609  brsset  23791  brtxpsd  23796  elfuns  23815  boxeq  24339  bnj1143  27855  lcvbr2  28363  atlrelat1  28662
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator