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

Theorem xchnxbir 310
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 205 . 2  |-  ( ph  <->  ch )
41, 3xchnxbi 309 1  |-  ( -. 
ch 
<->  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187
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 188
This theorem is referenced by:  3ioran  1000  hadnot  1500  cadnot  1513  nnelOLD  2771  nsspssun  3706  undif3  3734  intirr  5234  ordtri3or  5471  frxp  6914  ressuppssdif  6944  domunfican  7847  ssfin4  8741  lcmfunsnlem2lem1  14599  ncoprmlnprm  14665  symgfix2  17045  gsumdixp  17825  symgmatr01lem  19665  ppttop  20009  mdegleb  23000  strlem1  27889  isarchi  28494  bnj1189  29814  dfon3  30652  poimirlem18  31872  poimirlem21  31875  poimirlem30  31884  poimirlem31  31885  dvtanlemOLD  31905  ftc1anclem3  31933  hdmaplem4  35261  mapdh9a  35277  ifpnot23  36042  ifpdfxor  36051  ifpnim1  36061  ifpnim2  36063  2exanali  36595  oddneven  38486
  Copyright terms: Public domain W3C validator