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  890  3anor  981  nannan  1337  nannot  1339  nanbi  1340  truxortru  1415  truxorfal  1416  falxorfal  1418  nic-mpALT  1479  nic-axALT  1481  sban  2091  sbex  2176  necon3abii  2632  ne3anior  2719  inssdif0  3767  dtruALT  4545  dtruALT2  4557  dm0rn0  5077  brprcneu  5705  pmltpc  20956  cvbr2  25709  soseq  27737  brsset  27942  brtxpsd  27947  dffun10  27967  dfint3  28005  brub  28007  wl-nfeqfb  28392  frgrancvvdeqlem2  30650  pgrpgt2nabel  30799  lmod1zrnlvec  31033  bnj1143  31880  lcvbr2  32763  atlrelat1  33062
  Copyright terms: Public domain W3C validator