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

Theorem xchnxbir 333
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 223 . 2 (𝜑𝜒)
41, 3xchnxbi 332 1 𝜒𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205
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 206
This theorem is referenced by:  3ioran  1107  3ianor  1108  hadnot  1604  cadnot  1617  2exanali  1864  nelb  3223  nsspssun  4218  undif3  4251  2nreu  4402  intirr  6073  ordtri3or  6350  nf1const  7251  nf1oconst  7252  frxp  8059  ressuppssdif  8117  suppofssd  8135  naddcllem  8623  domunfican  9265  ssfin4  10247  prinfzo0  13612  swrdnnn0nd  14545  swrdnd0  14546  lcmfunsnlem2lem1  16515  ncoprmlnprm  16604  prm23ge5  16688  smndex2dnrinv  18726  symgfix2  19199  gsumdixp  20034  cnfldfun  20811  symgmatr01lem  22005  ppttop  22360  zclmncvs  24515  mdegleb  25432  2lgslem3  26755  trlsegvdeg  29174  strlem1  31195  difrab2  31429  isarchi  32021  bnj1189  33624  dfacycgr1  33741  fmlasucdisj  33996  dfon3  34480  wl-3xornot  35955  poimirlem18  36099  poimirlem21  36102  poimirlem30  36111  poimirlem31  36112  ftc1anclem3  36156  hdmaplem4  40240  mapdh9a  40255  onsupmaxb  41576  dflim5  41666  faosnf0.11b  41706  ifpnot23  41757  ifpdfxor  41766  ifpnim1  41776  ifpnim2  41778  dfsucon  41802  ntrneineine1lem  42363  disjrnmpt2  43414  aiotavb  45329  dfatprc  45369  ndmafv2nrn  45461  nfunsnafv2  45464  oddneven  45843
  Copyright terms: Public domain W3C validator