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 ) )

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  75  ancld  325  ancrd  326  anim12d  335  anim1d  336  anim2d  337  orel2  738  pm2.621  759  orim1d  799  orim2d  800  pm2.63  812  pm2.74  819  simprimdc  871  oplem1  988  equsex  1780  equsexd  1782  r19.36av  2702  r19.44av  2710  r19.45av  2711  reuss  3514  opthpr  3897  relop  4930  swoord2  6837  indpi  7709  lelttr  8414  elnnz  9658  ztri3or0  9690  xrlelttr  10218  icossicc  10372  iocssicc  10373  ioossico  10374  nn0sqdc  11160  issubassa3  15061  lmconst  15366  cnptopresti  15388  sslm  15397  bj-exlimmp  16895