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

Theorem xchbinx 301
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 287 . 2  |-  ( -. 
ps 
<->  -.  ch )
41, 3bitri 240 1  |-  ( ph  <->  -. 
ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176
This theorem is referenced by:  xchbinxr  302  con1bii  321  pm4.52  477  pm4.54  479  xordi  865  3anor  948  nannan  1291  nannot  1293  nanbi  1294  truxortru  1348  truxorfal  1349  falxorfal  1351  nic-mpALT  1427  nic-axALT  1429  sban  2009  sbex  2067  necon3abii  2476  ne3anior  2532  inssdif0  3521  dtruALT  4207  dtruALT2  4219  dm0rn0  4895  brprcneu  5518  pmltpc  18810  cvbr2  22863  soseq  24254  brsset  24429  brtxpsd  24434  boxeq  24987  bnj1143  28822  lcvbr2  29212  atlrelat1  29511
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 177
  Copyright terms: Public domain W3C validator