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  721  pm2.621  742  orim1d  782  orim2d  783  pm2.63  795  pm2.74  802  simprimdc  854  oplem1  970  equsex  1721  equsexd  1722  r19.36av  2621  r19.44av  2629  r19.45av  2630  reuss  3408  opthpr  3759  relop  4761  swoord2  6543  indpi  7304  lelttr  8008  elnnz  9222  ztri3or0  9254  xrlelttr  9763  icossicc  9917  iocssicc  9918  ioossico  9919  lmconst  13010  cnptopresti  13032  sslm  13041  bj-exlimmp  13804