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  726  pm2.621  747  orim1d  787  orim2d  788  pm2.63  800  pm2.74  807  simprimdc  859  oplem1  975  equsex  1728  equsexd  1729  r19.36av  2628  r19.44av  2636  r19.45av  2637  reuss  3417  opthpr  3773  relop  4778  swoord2  6565  indpi  7341  lelttr  8046  elnnz  9263  ztri3or0  9295  xrlelttr  9806  icossicc  9960  iocssicc  9961  ioossico  9962  lmconst  13719  cnptopresti  13741  sslm  13750  bj-exlimmp  14524