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  1095  3ianor  1096  hadnot  1689  cadnot  1702  nsspssun  4006  undif3  4037  intirr  5654  ordtri3or  5897  frxp  7442  ressuppssdif  7471  domunfican  8393  ssfin4  9338  prinfzo0  12715  lcmfunsnlem2lem1  15559  ncoprmlnprm  15643  prm23ge5  15727  symgfix2  18043  gsumdixp  18817  cnfldfunALT  19974  symgmatr01lem  20678  ppttop  21032  zclmncvs  23167  mdegleb  24044  2lgslem3  25350  trlsegvdeg  27407  strlem1  29449  isarchi  30076  bnj1189  31415  dfon3  32336  poimirlem18  33760  poimirlem21  33763  poimirlem30  33772  poimirlem31  33773  ftc1anclem3  33819  hdmaplem4  37584  mapdh9a  37599  ifpnot23  38349  ifpdfxor  38358  ifpnim1  38368  ifpnim2  38370  relintabex  38413  ntrneineine1lem  38908  2exanali  39113  oddneven  42082
  Copyright terms: Public domain W3C validator