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

Theorem xchnxbir 307
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 306 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  989  nnelOLD  2800  nsspssun  3728  undif3  3756  ordtri3or  4899  intirr  5373  frxp  6883  ressuppssdif  6913  domunfican  7785  ssfin4  8681  symgfix2  16640  gsumdixpOLD  17452  gsumdixp  17453  symgmatr01lem  19322  ppttop  19675  mdegleb  22630  strlem1  27367  isarchi  27960  dfon3  29770  dvtanlem  30304  ftc1anclem3  30332  2exanali  31534  oddneven  32558  bnj1189  34466  hdmaplem4  37898  mapdh9a  37914  ifpnot23  38119  ifpnim1  38123  ifpnim2  38124  ifpdfxor  38146
  Copyright terms: Public domain W3C validator