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  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  3892  relop  4925  swoord2  6827  indpi  7699  lelttr  8404  elnnz  9633  ztri3or0  9665  xrlelttr  10187  icossicc  10341  iocssicc  10342  ioossico  10343  lmconst  15240  cnptopresti  15262  sslm  15271  bj-exlimmp  16711