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  845  oplem1  960  equsex  1708  equsexd  1709  r19.36av  2608  r19.44av  2616  r19.45av  2617  reuss  3388  opthpr  3735  relop  4733  swoord2  6503  indpi  7245  lelttr  7948  elnnz  9160  ztri3or0  9192  xrlelttr  9692  icossicc  9846  iocssicc  9847  ioossico  9848  lmconst  12576  cnptopresti  12598  sslm  12607  bj-exlimmp  13303