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

Theorem xchbinx 310
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 296 . 2  |-  ( -. 
ps 
<->  -.  ch )
41, 3bitri 249 1  |-  ( ph  <->  -. 
ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  xchbinxr  311  con1bii  331  pm4.52  491  pm4.54  493  xordi  891  3anor  984  nannan  1342  nannot  1344  nanbi  1345  truxortru  1420  truxorfal  1421  falxorfal  1423  nic-mpALT  1484  nic-axALT  1486  sban  2107  sbex  2191  necon3abii  2720  ne3anior  2786  inssdif0  3887  dtruALT  4672  dtruALT2  4684  dm0rn0  5210  brprcneu  5850  pmltpc  21590  frgrancvvdeqlem2  24694  cvbr2  26864  soseq  28897  brsset  29102  brtxpsd  29107  dffun10  29127  dfint3  29165  brub  29167  wl-nfeqfb  29553  pgrpgt2nabl  31899  lmod1zrnlvec  32051  bnj1143  32803  lcvbr2  33694  atlrelat1  33993
  Copyright terms: Public domain W3C validator