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  9654  ztri3or0  9686  xrlelttr  10208  icossicc  10362  iocssicc  10363  ioossico  10364  issubassa3  15012  lmconst  15317  cnptopresti  15339  sslm  15348  bj-exlimmp  16797