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  867  3anor  950  nannan  1293  nannot  1295  nanbi  1296  truxortru  1350  truxorfal  1351  falxorfal  1353  nic-mpALT  1428  nic-axALT  1430  sban  2009  sbex  2071  necon3abii  2478  ne3anior  2534  inssdif0  3523  dtruALT  4207  dtruALT2  4219  dm0rn0  4895  pmltpc  18805  cvbr2  22856  soseq  23656  brsset  23838  brtxpsd  23843  elfuns  23862  boxeq  24386  bnj1143  28090  lcvbr2  28480  atlrelat1  28779
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