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

Theorem xchnxbir 309
Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
Hypotheses
Ref Expression
xchnxbir.1  |-  ( -. 
ph 
<->  ps )
xchnxbir.2  |-  ( ch  <->  ph )
Assertion
Ref Expression
xchnxbir  |-  ( -. 
ch 
<->  ps )

Proof of Theorem xchnxbir
StepHypRef Expression
1 xchnxbir.1 . 2  |-  ( -. 
ph 
<->  ps )
2 xchnxbir.2 . . 3  |-  ( ch  <->  ph )
32bicomi 202 . 2  |-  ( ph  <->  ch )
41, 3xchnxbi 308 1  |-  ( -. 
ch 
<->  ps )
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:  3ioran  991  nnelOLD  2813  nsspssun  3731  undif3  3759  ordtri3or  4910  intirr  5383  frxp  6890  ressuppssdif  6918  domunfican  7789  ssfin4  8686  wrdsymb0  12536  symgfix2  16236  gsumdixpOLD  17041  gsumdixp  17042  symgmatr01lem  18922  ppttop  19274  mdegleb  22199  strlem1  26845  isarchi  27388  dfon3  29119  dvtanlem  29641  ftc1anclem3  29669  2exanali  30871  bnj1189  33144  hdmaplem4  36571  mapdh9a  36587
  Copyright terms: Public domain W3C validator