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 224 . 2 (𝜑𝜒)
41, 3xchnxbi 332 1 𝜒𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206
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 207
This theorem is referenced by:  3ioran  1106  3ianor  1107  hadnot  1602  cadnot  1615  2exanali  1860  nabbib  3045  nelb  3234  nsspssun  4268  undif3  4300  2nreu  4444  intirr  6138  ordtri3or  6416  nf1const  7324  nf1oconst  7325  frxp  8151  ressuppssdif  8210  suppofssd  8228  naddcllem  8714  domunfican  9361  ssfin4  10350  prinfzo0  13738  swrdnnn0nd  14694  swrdnd0  14695  lcmfunsnlem2lem1  16675  ncoprmlnprm  16765  prm23ge5  16853  smndex2dnrinv  18928  symgfix2  19434  gsumdixp  20316  cnfldfun  21378  cnfldfunOLD  21391  symgmatr01lem  22659  ppttop  23014  zclmncvs  25182  mdegleb  26103  2lgslem3  27448  trlsegvdeg  30246  strlem1  32269  difrab2  32517  isarchi  33189  bnj1189  35023  dfacycgr1  35149  fmlasucdisj  35404  dfon3  35893  wl-3xornot  37482  poimirlem18  37645  poimirlem21  37648  poimirlem30  37657  poimirlem31  37658  ftc1anclem3  37702  hdmaplem4  41776  mapdh9a  41791  onsupmaxb  43251  dflim5  43342  faosnf0.11b  43440  ifpnot23  43491  ifpdfxor  43500  ifpnim1  43510  ifpnim2  43512  dfsucon  43536  ntrneineine1lem  44097  disjrnmpt2  45193  aiotavb  47102  dfatprc  47142  ndmafv2nrn  47234  nfunsnafv2  47237  oddneven  47631  usgrexmpl2trifr  47996
  Copyright terms: Public domain W3C validator