Theorem idd 25

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

Assertion

Ref	Expression
idd	⊢ (𝜑 → (𝜓 → 𝜓))

Proof of Theorem idd

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

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim1d  83  simprim  167  pm2.6  193  pm2.65  195  ancld  560  ancrd  561  anim12d  621  anim1d  623  anim2d  624  orel2  904  pm2.621  912  pm2.63  955  orim1d  981  orim2d  982  cad0  1651  merco2  1769  exgen  2009  spnfw  2014  r19.29vva  3226  rmosn  4680  opthpr  4809  opthprneg  4823  wereu2  5652  relop  5834  frpomin  6361  fpropnf1  7294  soxp  8168  omopth2  8620  swoord2  8779  mapdom2  9195  en3lplem2  9641  rankxplim3  9925  cfsmolem  10375  fin1a2s  10519  fpwwe2lem11  10753  fpwwe2lem12  10754  inawina  10802  gchina  10811  elnnz  12730  xmullem  13421  icossicc  13594  iocssicc  13595  ioossico  13596  ioopnfsup  14031  icopnfsup  14032  expeq0  14262  repswswrd  14963  repswcshw  14991  coprmprod  16865  vdwlem6  17193  lublecllem  18561  tsrlemax  18789  chnccat  18829  ablsimpnosubgd  20350  ocv2ss  22009  issubassa3  22204  0top  23331  neindisj2  23471  lmconst  23609  cnpresti  23636  sslm  23647  cmpfi  23756  dfconn2  23767  hausflim  24330  bndth  25309  nmoleub2a  25468  nmoleub2b  25469  cmetcaulem  25639  ioorf  25924  ioorinv2  25926  dvfsumlem2  26377  dgrcolem2  26623  plydiveu  26649  taylthlem2  26731  dvloglem  27006  elnnzs  28817  expsne0  28852  bdayfinbndlem1  28883  lmieu  29319  axcontlem4  29575  subgrpth  30386  clwwlknwwlksn  30659  numclwwlk1lem2foa  30985  dipsubdir  31480  rmo6  35780  mpofvd  35797  onprcf1acwevdlem1  36045  mirimanoffr  36627  mirimanofffr  36629  idinside  37027  endofsegid  37028  nn0prpwlem  37288  meran1  37377  onsuct0  37407  weiunso  37432  bj-axdd2ALT  37697  bj-sngltag  38074  poimirlem26  38756  ftc1anclem7  38809  fdc1  38872  rngosubdi  39071  rngosubdir  39072  mpobi123f  39286  lkreqN  40419  cdlemg33a  41955  mapdordlem2  42886  fimgmcyc  43791  onsucf1olem  44464  cnvtrucl0  44816  ntrneiiso  45283  3ornot23  45683  rspsbc2  45708  sbcim2g  45712  idn2  45787  idn3  45789  trsspwALT2  45992  sspwtrALT  45995  sstrALT2  46008  r19.36vf  46356  ioossioc  46709  ioossioobi  46734  stoweidlem27  47242  stoweidlem31  47246  stoweidlem60  47275  hoidmvlelem3  47812  chnerlem3  48099  atbiffatnnb  48187  cfsetsnfsetf1  48334  el1fzopredsuc  48601  poprelb  48811  isubgr3stgrlem4  49272  upwlkwlk  49442  line2y  50072  elsetrecslem  51072