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

Theorem xchnxbir 336
 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 227 . 2 (𝜑𝜒)
41, 3xchnxbi 335 1 𝜒𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209 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 210 This theorem is referenced by:  3ioran  1103  3ianor  1104  hadnot  1604  cadnot  1617  2exanali  1861  nsspssun  4184  undif3  4215  2nreu  4349  intirr  5945  ordtri3or  6191  nf1const  7038  nf1oconst  7039  frxp  7805  ressuppssdif  7836  suppofssd  7852  domunfican  8777  ssfin4  9723  prinfzo0  13073  swrdnnn0nd  14011  swrdnd0  14012  lcmfunsnlem2lem1  15974  ncoprmlnprm  16060  prm23ge5  16144  smndex2dnrinv  18074  symgfix2  18539  gsumdixp  19358  cnfldfunALT  20107  symgmatr01lem  21265  ppttop  21619  zclmncvs  23760  mdegleb  24672  2lgslem3  25995  trlsegvdeg  28019  strlem1  30040  difrab2  30275  isarchi  30868  bnj1189  32403  dfacycgr1  32516  fmlasucdisj  32771  dfon3  33478  wl-3xornot  34914  poimirlem18  35091  poimirlem21  35094  poimirlem30  35103  poimirlem31  35104  ftc1anclem3  35148  hdmaplem4  39086  mapdh9a  39101  ifpnot23  40201  ifpdfxor  40210  ifpnim1  40220  ifpnim2  40222  dfsucon  40246  ntrneineine1lem  40802  disjrnmpt2  41830  aiotavb  43662  dfatprc  43701  ndmafv2nrn  43793  nfunsnafv2  43796  oddneven  44177
 Copyright terms: Public domain W3C validator