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  983  nnelOLD  2791  nsspssun  3667  undif3  3695  ordtri3or  4835  intirr  5300  frxp  6768  ressuppssdif  6796  domunfican  7671  ssfin4  8566  wrdsymb0  12347  symgfix2  16009  gsumdixpOLD  16792  gsumdixp  16793  symgmatr01lem  18561  ppttop  18713  mdegleb  21637  strlem1  25775  isarchi  26319  dfon3  28043  dvtanlem  28565  ftc1anclem3  28593  2exanali  29764  bnj1189  32282  hdmaplem4  35701  mapdh9a  35717
  Copyright terms: Public domain W3C validator