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  169  pm2.6  194  pm2.65  196  ancld  554  ancrd  555  anim12d  611  anim1d  613  anim2d  614  orel2  888  pm2.621  896  pm2.63  938  orim1d  963  orim2d  964  ecase2d  1027  cad0  1619  merco2  1738  exgen  1978  spnfw  1984  rmosn  4629  opthpr  4755  opthprneg  4768  wereu2  5529  relop  5698  fpropnf1  7008  soxp  7810  omopth2  8197  swoord2  8308  mapdom2  8676  en3lplem2  9064  rankxplim3  9298  cfsmolem  9681  fin1a2s  9825  fpwwe2lem12  10052  fpwwe2lem13  10053  inawina  10101  gchina  10110  elnnz  11979  xmullem  12645  icossicc  12814  iocssicc  12815  ioossico  12816  ioopnfsup  13227  icopnfsup  13228  expeq0  13455  repswswrd  14137  repswcshw  14165  coprmprod  15994  vdwlem6  16311  lublecllem  17589  tsrlemax  17821  ablsimpnosubgd  19217  ocv2ss  20360  issubassa3  20552  0top  21586  neindisj2  21726  lmconst  21864  cnpresti  21891  sslm  21902  cmpfi  22011  dfconn2  22022  hausflim  22584  bndth  23561  nmoleub2a  23720  nmoleub2b  23721  cmetcaulem  23890  ioorf  24175  ioorinv2  24177  dgrcolem2  24869  plydiveu  24892  dvloglem  25237  lmieu  26576  axcontlem4  26759  clwwlknwwlksn  27821  numclwwlk1lem2foa  28137  dipsubdir  28629  omssubadd  31632  subgrpth  32455  frpomin  33152  idinside  33619  endofsegid  33620  nn0prpwlem  33744  meran1  33833  onsuct0  33863  bj-sngltag  34380  poimirlem26  35041  ftc1anclem7  35094  fdc1  35142  rngosubdi  35341  rngosubdir  35342  mpobi123f  35558  lkreqN  36424  cdlemg33a  37960  mapdordlem2  38891  cnvtrucl0  40254  ntrneiiso  40727  3ornot23  41149  rspsbc2  41174  sbcim2g  41178  idn2  41253  idn3  41255  trsspwALT2  41459  sspwtrALT  41462  sstrALT2  41475  r19.36vf  41709  ioossioc  42068  ioossioobi  42093  stoweidlem27  42608  stoweidlem31  42612  stoweidlem60  42641  hoidmvlelem3  43175  atbiffatnnb  43444  el1fzopredsuc  43821  poprelb  43980  upwlkwlk  44306  line2y  45108  elsetrecslem  45167
  Copyright terms: Public domain W3C validator