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  2022  sbex  2080  necon3abii  2489  ne3anior  2545  inssdif0  3534  dtruALT  4223  dtruALT2  4235  dm0rn0  4911  brprcneu  5534  pmltpc  18826  cvbr2  22879  soseq  24325  brsset  24500  brtxpsd  24505  boxeq  25090  bnj1143  29138  sbanNEW7  29544  sbexNEW7  29589  lcvbr2  29834  atlrelat1  30133
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