MPE Home 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 214 . 2 (𝜑𝜒)
41, 3xchnxbi 321 1 𝜒𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196
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 197
This theorem is referenced by:  3ioran  1073  3ianor  1074  hadnot  1581  cadnot  1594  nsspssun  3890  undif3  3921  undif3OLD  3922  intirr  5549  ordtri3or  5793  frxp  7332  ressuppssdif  7361  domunfican  8274  ssfin4  9170  prinfzo0  12546  lcmfunsnlem2lem1  15398  ncoprmlnprm  15483  prm23ge5  15567  symgfix2  17882  gsumdixp  18655  cnfldfunALT  19807  symgmatr01lem  20507  ppttop  20859  zclmncvs  22994  mdegleb  23869  2lgslem3  25174  trlsegvdeg  27205  strlem1  29237  isarchi  29864  bnj1189  31203  dfon3  32124  poimirlem18  33557  poimirlem21  33560  poimirlem30  33569  poimirlem31  33570  ftc1anclem3  33617  hdmaplem4  37380  mapdh9a  37396  ifpnot23  38140  ifpdfxor  38149  ifpnim1  38159  ifpnim2  38161  relintabex  38204  ntrneineine1lem  38699  2exanali  38904  oddneven  41882
  Copyright terms: Public domain W3C validator