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

Theorem xchnxbir 322
 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 213 . 2 (𝜑𝜒)
41, 3xchnxbi 321 1 𝜒𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195 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 196 This theorem is referenced by:  3ioran  1049  hadnot  1532  cadnot  1545  nsspssun  3819  undif3  3847  undif3OLD  3848  intirr  5433  ordtri3or  5672  frxp  7174  ressuppssdif  7203  domunfican  8118  ssfin4  9015  lcmfunsnlem2lem1  15189  ncoprmlnprm  15274  prm23ge5  15358  symgfix2  17659  gsumdixp  18432  symgmatr01lem  20278  ppttop  20621  zclmncvs  22756  mdegleb  23628  2lgslem3  24929  strlem1  28493  isarchi  29067  bnj1189  30331  dfon3  31169  poimirlem18  32597  poimirlem21  32600  poimirlem30  32609  poimirlem31  32610  ftc1anclem3  32657  hdmaplem4  36081  mapdh9a  36097  ifpnot23  36842  ifpdfxor  36851  ifpnim1  36861  ifpnim2  36863  relintabex  36906  ntrneineine1lem  37402  2exanali  37609  oddneven  40095  prinfzo0  40363  trlsegvdeg  41395
 Copyright terms: Public domain W3C validator