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

Theorem xchnxbir 321
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 212 . 2 (𝜑𝜒)
41, 3xchnxbi 320 1 𝜒𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194
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 195
This theorem is referenced by:  3ioran  1048  hadnot  1531  cadnot  1544  nsspssun  3818  undif3  3846  undif3OLD  3847  intirr  5419  ordtri3or  5657  frxp  7151  ressuppssdif  7180  domunfican  8095  ssfin4  8992  lcmfunsnlem2lem1  15137  ncoprmlnprm  15222  prm23ge5  15306  symgfix2  17607  gsumdixp  18380  symgmatr01lem  20225  ppttop  20568  mdegleb  23572  2lgslem3  24873  strlem1  28286  isarchi  28860  bnj1189  30124  dfon3  30962  poimirlem18  32380  poimirlem21  32383  poimirlem30  32392  poimirlem31  32393  ftc1anclem3  32440  hdmaplem4  35864  mapdh9a  35880  ifpnot23  36625  ifpdfxor  36634  ifpnim1  36644  ifpnim2  36646  relintabex  36689  ntrneineine1lem  37185  2exanali  37392  oddneven  39879  prinfzo0  40169  trlsegvdeg  41376
  Copyright terms: Public domain W3C validator