Theorem idd 24

Description: Principle of identity with antecedent. (Contributed by NM, 26-Nov-1995.)

Assertion

Ref	Expression
idd

Proof of Theorem idd

Step	Hyp	Ref	Expression
1		id 22	. 2
2	1	a1i 11	1

Syntax hints:  ->wi 4

This theorem is referenced by:  imim1d  75  simprim  150  pm2.6  170  pm2.65  172  orel2  383  pm2.621  408  simpr  461  ancld  553  ancrd  554  anim12d  563  anim1d  564  anim2d  565  pm2.63  788  orim1d  839  orim2d  840  ecase2d  940  cad0  1467  merco2  1569  spnfw  1785  r19.36v  3005  r19.44v  3014  r19.45v  3015  eqsbc3r  3389  reuss  3778  opthpr  4208  wereu2  4881  relop  5158  soxp  6913  omopth2  7252  swoord2  7360  mapdom2  7708  en3lplem2  8053  rankxplim3  8320  cfsmolem  8671  fin1a2s  8815  fpwwe2lem12  9040  fpwwe2lem13  9041  inawina  9089  gchina  9098  elnnz  10899  xmullem  11485  icossicc  11640  iocssicc  11641  ioossico  11642  ioopnfsup  11991  icopnfsup  11992  expeq0  12196  repswswrd  12756  repswcshw  12780  vdwlem6  14504  lublecllem  15618  tsrlemax  15850  ocv2ss  18704  0top  19485  neindisj2  19624  lmconst  19762  cnpresti  19789  sslm  19800  cmpfi  19908  bwthOLD  19911  dfcon2  19920  hausflim  20482  bndth  21458  nmoleub2a  21600  nmoleub2b  21601  cmetcaulem  21727  ioorf  21982  ioorinv2  21984  dgrcolem2  22671  plydiveu  22694  dvloglem  23029  lmieu  24150  axcontlem4  24270  grponnncan2  25256  dipsubdir  25763  idinside  29734  endofsegid  29735  meran1  29876  onsuct0  29906  ftc1anclem7  30096  nn0prpwlem  30140  nn0prpw  30141  fdc1  30239  rngosubdi  30356  rngosubdir  30357  mpt2bi123f  30571  ioossioc  31524  ioossioobi  31557  stoweidlem27  31809  stoweidlem31  31813  stoweidlem60  31842  atbiffatnnb  32108  3ornot23  33278  rspsbc2  33305  sbcim2g  33309  idn2  33399  idn3  33401  trsspwALT2  33617  sspwtrALT  33620  sstrALT2  33635  bj-sngltag  34541  lkreqN  34895  cdlemg33a  36432  mapdordlem2  37364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7