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-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  imim1d  75  ancld  323  ancrd  324  anim12d  333  anim1d  334  anim2d  335  orel2  715  pm2.621  736  orim1d  776  orim2d  777  pm2.63  789  pm2.74  796  simprimdc  844  oplem1  959  equsex  1706  equsexd  1707  r19.36av  2582  r19.44av  2590  r19.45av  2591  reuss  3357  opthpr  3699  relop  4689  swoord2  6459  indpi  7150  lelttr  7852  elnnz  9064  ztri3or0  9096  xrlelttr  9589  icossicc  9743  iocssicc  9744  ioossico  9745  lmconst  12385  cnptopresti  12407  sslm  12416  bj-exlimmp  12976