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  728  pm2.621  749  orim1d  789  orim2d  790  pm2.63  802  pm2.74  809  simprimdc  861  oplem1  978  equsex  1751  equsexd  1752  r19.36av  2657  r19.44av  2665  r19.45av  2666  reuss  3454  opthpr  3813  relop  4828  swoord2  6650  indpi  7455  lelttr  8161  elnnz  9382  ztri3or0  9414  xrlelttr  9928  icossicc  10082  iocssicc  10083  ioossico  10084  lmconst  14688  cnptopresti  14710  sslm  14719  bj-exlimmp  15705