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  1554  merco2  1659  spnfw  1926  eqsbc3rOLD  3487  opthpr  4375  wereu2  5101  relop  5261  fpropnf1  6509  soxp  7275  omopth2  7649  swoord2  7759  mapdom2  8116  en3lplem2  8497  rankxplim3  8729  cfsmolem  9077  fin1a2s  9221  fpwwe2lem12  9448  fpwwe2lem13  9449  inawina  9497  gchina  9506  elnnz  11372  xmullem  12079  icossicc  12245  iocssicc  12246  ioossico  12247  ioopnfsup  12646  icopnfsup  12647  expeq0  12873  repswswrd  13512  repswcshw  13539  coprmprod  15356  vdwlem6  15671  lublecllem  16969  tsrlemax  17201  ocv2ss  19998  0top  20768  neindisj2  20908  lmconst  21046  cnpresti  21073  sslm  21084  cmpfi  21192  dfconn2  21203  hausflim  21766  bndth  22738  nmoleub2a  22898  nmoleub2b  22899  cmetcaulem  23067  ioorf  23322  ioorinv2  23324  dgrcolem2  24011  plydiveu  24034  dvloglem  24375  lmieu  25657  axcontlem4  25828  dipsubdir  27673  omssubadd  30336  idinside  32166  endofsegid  32167  nn0prpwlem  32292  nn0prpw  32293  meran1  32385  onsuct0  32415  bj-sngltag  32946  poimirlem26  33406  ftc1anclem7  33462  fdc1  33513  rngosubdi  33715  rngosubdir  33716  mpt2bi123f  33942  lkreqN  34276  cdlemg33a  35813  mapdordlem2  36745  cnvtrucl0  37750  ntrneiiso  38209  3ornot23  38535  rspsbc2  38564  sbcim2g  38568  idn2  38658  idn3  38660  trsspwALT2  38866  sspwtrALT  38869  sstrALT2  38890  r19.36vf  39144  ioossioc  39516  ioossioobi  39546  stoweidlem27  40007  stoweidlem31  40011  stoweidlem60  40040  hoidmvlelem3  40574  atbiffatnnb  40842  el1fzopredsuc  41098  upwlkwlk  41485  elsetrecslem  42209
  Copyright terms: Public domain W3C validator