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  75  ancld  321  ancrd  322  anim12d  331  anim1d  332  anim2d  333  orel2  698  pm2.621  719  orim1d  759  orim2d  760  pm2.63  772  pm2.74  779  simprimdc  825  oplem1  940  equsex  1687  equsexd  1688  r19.36av  2554  r19.44av  2562  r19.45av  2563  reuss  3321  opthpr  3663  relop  4647  swoord2  6411  indpi  7092  lelttr  7769  elnnz  8962  ztri3or0  8994  xrlelttr  9476  icossicc  9630  iocssicc  9631  ioossico  9632  lmconst  12221  cnptopresti  12243  sslm  12252  bj-exlimmp  12660