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  166  pm2.6  190  pm2.65  192  ancld  552  ancrd  553  anim12d  610  anim1d  612  anim2d  613  orel2  890  pm2.621  898  pm2.63  940  orim1d  965  orim2d  966  ecase2dOLD  1030  cad0  1620  cad0OLD  1621  merco2  1739  exgen  1979  spnfw  1984  r19.29vva  3208  ab0w  4334  rmosn  4681  opthpr  4810  opthprneg  4823  wereu2  5631  relop  5807  frpomin  6295  fpropnf1  7215  soxp  8062  omopth2  8532  swoord2  8681  mapdom2  9093  en3lplem2  9550  rankxplim3  9818  cfsmolem  10207  fin1a2s  10351  fpwwe2lem11  10578  fpwwe2lem12  10579  inawina  10627  gchina  10636  elnnz  12510  xmullem  13184  icossicc  13354  iocssicc  13355  ioossico  13356  ioopnfsup  13770  icopnfsup  13771  expeq0  13999  repswswrd  14673  repswcshw  14701  coprmprod  16538  vdwlem6  16859  lublecllem  18250  tsrlemax  18476  ablsimpnosubgd  19884  ocv2ss  21080  issubassa3  21274  0top  22336  neindisj2  22477  lmconst  22615  cnpresti  22642  sslm  22653  cmpfi  22762  dfconn2  22773  hausflim  23335  bndth  24324  nmoleub2a  24483  nmoleub2b  24484  cmetcaulem  24655  ioorf  24940  ioorinv2  24942  dgrcolem2  25638  plydiveu  25661  dvloglem  26006  lmieu  27729  axcontlem4  27919  clwwlknwwlksn  28985  numclwwlk1lem2foa  29301  dipsubdir  29793  fldgenid  32089  omssubadd  32903  subgrpth  33731  idinside  34672  endofsegid  34673  nn0prpwlem  34797  meran1  34886  onsuct0  34916  bj-sngltag  35457  poimirlem26  36107  ftc1anclem7  36160  fdc1  36208  rngosubdi  36407  rngosubdir  36408  mpobi123f  36624  lkreqN  37635  cdlemg33a  39172  mapdordlem2  40103  onsucf1olem  41608  cnvtrucl0  41903  ntrneiiso  42370  3ornot23  42798  rspsbc2  42823  sbcim2g  42827  idn2  42902  idn3  42904  trsspwALT2  43108  sspwtrALT  43111  sstrALT2  43124  r19.36vf  43353  ioossioc  43737  ioossioobi  43762  stoweidlem27  44275  stoweidlem31  44279  stoweidlem60  44308  hoidmvlelem3  44845  atbiffatnnb  45154  cfsetsnfsetf1  45300  el1fzopredsuc  45564  poprelb  45723  upwlkwlk  46048  line2y  46848  elsetrecslem  47151
  Copyright terms: Public domain W3C validator