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  1752  equsexd  1753  r19.36av  2659  r19.44av  2667  r19.45av  2668  reuss  3462  opthpr  3826  relop  4846  swoord2  6673  indpi  7490  lelttr  8196  elnnz  9417  ztri3or0  9449  xrlelttr  9963  icossicc  10117  iocssicc  10118  ioossico  10119  lmconst  14803  cnptopresti  14825  sslm  14834  bj-exlimmp  15905