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

Theorem xchnxbir 332
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 331 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  1106  3ianor  1107  hadnot  1603  cadnot  1616  2exanali  1863  nelb  3222  nsspssun  4217  undif3  4250  2nreu  4401  intirr  6072  ordtri3or  6349  nf1const  7249  nf1oconst  7250  frxp  8057  ressuppssdif  8115  suppofssd  8133  naddcllem  8621  domunfican  9263  ssfin4  10245  prinfzo0  13610  swrdnnn0nd  14543  swrdnd0  14544  lcmfunsnlem2lem1  16513  ncoprmlnprm  16602  prm23ge5  16686  smndex2dnrinv  18724  symgfix2  19196  gsumdixp  20031  cnfldfun  20806  symgmatr01lem  22000  ppttop  22355  zclmncvs  24510  mdegleb  25427  2lgslem3  26750  trlsegvdeg  29169  strlem1  31190  difrab2  31424  isarchi  32013  bnj1189  33612  dfacycgr1  33729  fmlasucdisj  33984  dfon3  34468  wl-3xornot  35943  poimirlem18  36087  poimirlem21  36090  poimirlem30  36099  poimirlem31  36100  ftc1anclem3  36144  hdmaplem4  40228  mapdh9a  40243  onsupmaxb  41551  dflim5  41641  faosnf0.11b  41681  ifpnot23  41732  ifpdfxor  41741  ifpnim1  41751  ifpnim2  41753  dfsucon  41777  ntrneineine1lem  42338  disjrnmpt2  43383  aiotavb  45294  dfatprc  45334  ndmafv2nrn  45426  nfunsnafv2  45429  oddneven  45808
  Copyright terms: Public domain W3C validator