MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xchnxbir 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
xchnxbir.2
Assertion
Ref Expression
xchnxbir

Proof of Theorem xchnxbir
StepHypRef Expression
1 xchnxbir.1 . 2
2 xchnxbir.2 . . 3
32bicomi 202 . 2
41, 3xchnxbi 308 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184
This theorem is referenced by:  3ioran  991  nnelOLD  2803  nsspssun  3730  undif3  3758  ordtri3or  4915  intirr  5390  frxp  6910  ressuppssdif  6940  domunfican  7813  ssfin4  8711  wrdsymb0  12575  symgfix2  16441  gsumdixpOLD  17257  gsumdixp  17258  symgmatr01lem  19155  ppttop  19508  mdegleb  22464  strlem1  27169  isarchi  27726  dfon3  29542  dvtanlem  30064  ftc1anclem3  30092  2exanali  31293  bnj1189  34065  hdmaplem4  37501  mapdh9a  37517  bj-ifnot23  37718  bj-ifdfxor  37732
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
  Copyright terms: Public domain W3C validator