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  4932  swoord2  6841  indpi  7715  lelttr  8420  elnnz  9665  ztri3or0  9697  xrlelttr  10225  icossicc  10379  iocssicc  10380  ioossico  10381  nn0sqdc  11168  issubassa3  15121  lmconst  15442  cnptopresti  15464  sslm  15473  bj-exlimmp  17002