Theorem idd 21

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

Assertion

Ref	Expression
idd	|- ( ph -> ( ps -> ps ) )

Proof of Theorem idd

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ps -> ps )
2	1	a1i 9	1 |- ( ph -> ( ps -> ps ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  imim1d  74  ancld  318  ancrd  319  anim12d  328  anim1d  329  anim2d  330  orel2  678  pm2.621  699  orim1d  734  orim2d  735  pm2.63  747  pm2.74  754  simprimdc  790  oplem1  917  equsex  1657  equsexd  1658  r19.36av  2506  r19.44av  2514  r19.45av  2515  reuss  3252  opthpr  3572  relop  4514  swoord2  6202  indpi  6594  lelttr  7266  elnnz  8442  ztri3or0  8474  xrlelttr  8952  icossicc  9059  iocssicc  9060  ioossico  9061  bj-exlimmp  10731