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  1961  sbex  2088  necon3abii  2442  ne3anior  2498  inssdif0  3427  dtruALT  4101  dtruALT2  4113  dm0rn0  4802  pmltpc  18642  cvbr2  22693  soseq  23422  brsset  23604  brtxpsd  23609  elfuns  23628  boxeq  24152  bnj1143  27511  lcvbr2  27901  atlrelat1  28200
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