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  3463  dtruALT  4145  dtruALT2  4157  dm0rn0  4848  pmltpc  18737  cvbr2  22788  soseq  23588  brsset  23770  brtxpsd  23775  elfuns  23794  boxeq  24318  bnj1143  27834  lcvbr2  28342  atlrelat1  28641
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