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  162  pm2.6  182  pm2.65  184  orel2  398  pm2.621  424  simpr  477  ancld  575  ancrd  576  anim12d  585  anim1d  587  anim2d  588  pm2.63  828  orim1d  883  orim2d  884  ecase2d  980  cad0  1553  merco2  1658  spnfw  1925  eqsbc3rOLD  3479  opthpr  4357  wereu2  5076  relop  5237  fpropnf1  6484  soxp  7242  omopth2  7616  swoord2  7726  mapdom2  8083  en3lplem2  8464  rankxplim3  8696  cfsmolem  9044  fin1a2s  9188  fpwwe2lem12  9415  fpwwe2lem13  9416  inawina  9464  gchina  9473  elnnz  11339  xmullem  12045  icossicc  12210  iocssicc  12211  ioossico  12212  ioopnfsup  12611  icopnfsup  12612  expeq0  12838  repswswrd  13476  repswcshw  13503  coprmprod  15310  vdwlem6  15625  lublecllem  16920  tsrlemax  17152  ocv2ss  19949  0top  20711  neindisj2  20850  lmconst  20988  cnpresti  21015  sslm  21026  cmpfi  21134  dfconn2  21145  hausflim  21708  bndth  22680  nmoleub2a  22840  nmoleub2b  22841  cmetcaulem  23009  ioorf  23264  ioorinv2  23266  dgrcolem2  23951  plydiveu  23974  dvloglem  24311  lmieu  25593  axcontlem4  25764  dipsubdir  27573  omssubadd  30167  idinside  31868  endofsegid  31869  nn0prpwlem  31994  nn0prpw  31995  meran1  32087  onsuct0  32117  bj-sngltag  32653  poimirlem26  33102  ftc1anclem7  33158  fdc1  33209  rngosubdi  33411  rngosubdir  33412  mpt2bi123f  33638  lkreqN  33972  cdlemg33a  35509  mapdordlem2  36441  cnvtrucl0  37447  ntrneiiso  37906  3ornot23  38232  rspsbc2  38261  sbcim2g  38265  idn2  38355  idn3  38357  trsspwALT2  38564  sspwtrALT  38567  sstrALT2  38588  r19.36vf  38846  ioossioc  39155  ioossioobi  39185  stoweidlem27  39577  stoweidlem31  39581  stoweidlem60  39610  hoidmvlelem3  40144  atbiffatnnb  40409  el1fzopredsuc  40658  upwlkwlk  41034  elsetrecslem  41763
  Copyright terms: Public domain W3C validator