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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	a1i 11	1 ⊢ (𝜑 → (𝜓 → 𝜓))

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  192  pm2.65  194  ancld  558  ancrd  559  anim12d  618  anim1d  620  anim2d  621  orel2  901  pm2.621  909  pm2.63  953  orim1d  978  orim2d  979  cad0  1637  merco2  1755  exgen  1993  spnfw  1998  r19.29vva  3221  rmosn  4677  opthpr  4808  opthprneg  4822  wereu2  5642  relop  5820  frpomin  6323  fpropnf1  7247  soxp  8104  omopth2  8548  swoord2  8707  mapdom2  9116  en3lplem2  9565  rankxplim3  9836  cfsmolem  10224  fin1a2s  10368  fpwwe2lem11  10596  fpwwe2lem12  10597  inawina  10645  gchina  10654  elnnz  12575  xmullem  13264  icossicc  13437  iocssicc  13438  ioossico  13439  ioopnfsup  13871  icopnfsup  13872  expeq0  14102  repswswrd  14794  repswcshw  14822  coprmprod  16678  vdwlem6  17005  lublecllem  18373  tsrlemax  18601  chnccat  18641  ablsimpnosubgd  20129  ocv2ss  21705  issubassa3  21898  0top  23023  neindisj2  23163  lmconst  23301  cnpresti  23328  sslm  23339  cmpfi  23448  dfconn2  23459  hausflim  24021  bndth  25000  nmoleub2a  25159  nmoleub2b  25160  cmetcaulem  25330  ioorf  25615  ioorinv2  25617  dvfsumlem2  26069  dgrcolem2  26314  plydiveu  26339  taylthlem2  26414  dvloglem  26690  elnnzs  28471  expsne0  28506  bdayfinbndlem1  28537  lmieu  28930  axcontlem4  29114  clwwlknwwlksn  30186  numclwwlk1lem2foa  30502  dipsubdir  30997  omssubadd  34558  subgrpth  35448  idinside  36398  endofsegid  36399  nn0prpwlem  36646  meran1  36735  onsuct0  36765  weiunso  36790  bj-axdd2ALT  37056  bj-sngltag  37432  poimirlem26  38109  ftc1anclem7  38162  fdc1  38209  rngosubdi  38408  rngosubdir  38409  mpobi123f  38625  lkreqN  39758  cdlemg33a  41294  mapdordlem2  42225  fimgmcyc  43116  onsucf1olem  43811  cnvtrucl0  44164  ntrneiiso  44631  3ornot23  45049  rspsbc2  45074  sbcim2g  45078  idn2  45153  idn3  45155  trsspwALT2  45358  sspwtrALT  45361  sstrALT2  45374  r19.36vf  45678  ioossioc  46032  ioossioobi  46057  stoweidlem27  46565  stoweidlem31  46569  stoweidlem60  46598  hoidmvlelem3  47135  chnerlem3  47424  atbiffatnnb  47470  cfsetsnfsetf1  47617  el1fzopredsuc  47884  poprelb  48094  isubgr3stgrlem4  48555  upwlkwlk  48725  line2y  49341  elsetrecslem  50284