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

Theorem idd 24
Description: Principle of identity id 22 with antecedent. (Contributed by NM, 26-Nov-1995.)
Assertion
Ref Expression
idd (𝜑 → (𝜓𝜓))

Proof of Theorem idd
StepHypRef Expression
1 id 22 . 2 (𝜓𝜓)
21a1i 11 1 (𝜑 → (𝜓𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  imim1d  82  simprim  167  pm2.6  192  pm2.65  194  ancld  551  ancrd  552  anim12d  608  anim1d  610  anim2d  611  orel2  884  pm2.621  892  pm2.63  934  orim1d  959  orim2d  960  ecase2d  1023  cad0  1609  merco2  1728  exgen  1969  spnfw  1975  rmosn  4649  opthpr  4776  opthprneg  4789  wereu2  5546  relop  5715  fpropnf1  7016  soxp  7814  omopth2  8200  swoord2  8311  mapdom2  8677  en3lplem2  9065  rankxplim3  9299  cfsmolem  9681  fin1a2s  9825  fpwwe2lem12  10052  fpwwe2lem13  10053  inawina  10101  gchina  10110  elnnz  11980  xmullem  12647  icossicc  12814  iocssicc  12815  ioossico  12816  ioopnfsup  13222  icopnfsup  13223  expeq0  13449  repswswrd  14136  repswcshw  14164  coprmprod  15995  vdwlem6  16312  lublecllem  17588  tsrlemax  17820  ablsimpnosubgd  19157  issubassa3  20027  ocv2ss  20747  0top  21521  neindisj2  21661  lmconst  21799  cnpresti  21826  sslm  21837  cmpfi  21946  dfconn2  21957  hausflim  22519  bndth  23491  nmoleub2a  23650  nmoleub2b  23651  cmetcaulem  23820  ioorf  24103  ioorinv2  24105  dgrcolem2  24793  plydiveu  24816  dvloglem  25158  lmieu  26498  axcontlem4  26681  clwwlknwwlksn  27744  numclwwlk1lem2foa  28061  dipsubdir  28553  omssubadd  31458  subgrpth  32279  frpomin  32976  idinside  33443  endofsegid  33444  nn0prpwlem  33568  meran1  33657  onsuct0  33687  bj-sngltag  34193  poimirlem26  34800  ftc1anclem7  34855  fdc1  34904  rngosubdi  35106  rngosubdir  35107  mpobi123f  35323  lkreqN  36188  cdlemg33a  37724  mapdordlem2  38655  cnvtrucl0  39864  ntrneiiso  40321  3ornot23  40723  rspsbc2  40748  sbcim2g  40752  idn2  40827  idn3  40829  trsspwALT2  41033  sspwtrALT  41036  sstrALT2  41049  r19.36vf  41284  ioossioc  41646  ioossioobi  41673  stoweidlem27  42193  stoweidlem31  42197  stoweidlem60  42226  hoidmvlelem3  42760  atbiffatnnb  43029  el1fzopredsuc  43406  poprelb  43533  upwlkwlk  43861  line2y  44640  elsetrecslem  44699
  Copyright terms: Public domain W3C validator