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  163  pm2.6  182  pm2.65  184  simprOLD  472  ancld  532  ancrd  533  anim12d  588  anim1d  590  anim2d  591  orel2  859  pm2.621  864  pm2.63  941  orim1d  946  orim2d  947  ecase2d  1016  cad0  1703  merco2  1808  spnfw  2085  opthpr  4513  opthprneg  4529  wereu2  5246  relop  5411  fpropnf1  6666  soxp  7440  omopth2  7817  swoord2  7927  mapdom2  8286  en3lplem2  8671  rankxplim3  8907  cfsmolem  9293  fin1a2s  9437  fpwwe2lem12  9664  fpwwe2lem13  9665  inawina  9713  gchina  9722  elnnz  11588  xmullem  12298  icossicc  12465  iocssicc  12466  ioossico  12467  ioopnfsup  12870  icopnfsup  12871  expeq0  13096  repswswrd  13739  repswcshw  13766  coprmprod  15581  vdwlem6  15896  lublecllem  17195  tsrlemax  17427  ocv2ss  20233  0top  21007  neindisj2  21147  lmconst  21285  cnpresti  21312  sslm  21323  cmpfi  21431  dfconn2  21442  hausflim  22004  bndth  22976  nmoleub2a  23135  nmoleub2b  23136  cmetcaulem  23304  ioorf  23560  ioorinv2  23562  dgrcolem2  24249  plydiveu  24272  dvloglem  24614  lmieu  25896  axcontlem4  26067  clwwlknwwlksn  27190  clwwlknwwlksnOLD  27191  clwwlknonwwlknonb  27278  numclwlk1lem2foa  27538  dipsubdir  28037  omssubadd  30696  frpomin  32069  idinside  32522  endofsegid  32523  nn0prpwlem  32648  nn0prpw  32649  meran1  32741  onsuct0  32771  bj-sngltag  33296  poimirlem26  33761  ftc1anclem7  33816  fdc1  33867  rngosubdi  34069  rngosubdir  34070  mpt2bi123f  34296  lkreqN  34972  cdlemg33a  36508  mapdordlem2  37440  cnvtrucl0  38450  ntrneiiso  38908  3ornot23  39234  rspsbc2  39263  sbcim2g  39267  idn2  39357  idn3  39359  trsspwALT2  39565  sspwtrALT  39568  sstrALT2  39586  r19.36vf  39839  ioossioc  40228  ioossioobi  40256  stoweidlem27  40755  stoweidlem31  40759  stoweidlem60  40788  hoidmvlelem3  41325  atbiffatnnb  41593  el1fzopredsuc  41853  upwlkwlk  42238  elsetrecslem  42963
  Copyright terms: Public domain W3C validator