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

Theorem xchnxbir 334
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 225 . 2 (𝜑𝜒)
41, 3xchnxbi 333 1 𝜒𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207
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 208
This theorem is referenced by:  3ioran  1100  3ianor  1101  hadnot  1596  cadnot  1609  2exanali  1853  nsspssun  4237  undif3  4268  2nreu  4395  intirr  5975  ordtri3or  6220  frxp  7814  ressuppssdif  7845  suppofssd  7861  domunfican  8783  ssfin4  9724  prinfzo0  13069  swrdnnn0nd  14011  swrdnd0  14012  lcmfunsnlem2lem1  15974  ncoprmlnprm  16060  prm23ge5  16144  symgfix2  18466  gsumdixp  19281  cnfldfunALT  20474  symgmatr01lem  21178  ppttop  21531  zclmncvs  23667  mdegleb  24573  2lgslem3  25894  trlsegvdeg  27920  strlem1  29941  difrab2  30175  isarchi  30725  bnj1189  32165  dfacycgr1  32275  fmlasucdisj  32530  dfon3  33237  poimirlem18  34777  poimirlem21  34780  poimirlem30  34789  poimirlem31  34790  ftc1anclem3  34836  hdmaplem4  38777  mapdh9a  38792  ifpnot23  39705  ifpdfxor  39714  ifpnim1  39724  ifpnim2  39726  dfsucon  39750  ntrneineine1lem  40295  disjrnmpt2  41310  aiotavb  43152  dfatprc  43191  ndmafv2nrn  43283  nfunsnafv2  43286  oddneven  43637
  Copyright terms: Public domain W3C validator