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  323  ancrd  324  anim12d  333  anim1d  334  anim2d  335  orel2  716  pm2.621  737  orim1d  777  orim2d  778  pm2.63  790  pm2.74  797  simprimdc  849  oplem1  965  equsex  1716  equsexd  1717  r19.36av  2617  r19.44av  2625  r19.45av  2626  reuss  3403  opthpr  3752  relop  4754  swoord2  6531  indpi  7283  lelttr  7987  elnnz  9201  ztri3or0  9233  xrlelttr  9742  icossicc  9896  iocssicc  9897  ioossico  9898  lmconst  12856  cnptopresti  12878  sslm  12887  bj-exlimmp  13650