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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  imim1d  74  ancld  318  ancrd  319  anim12d  328  anim1d  329  anim2d  330  orel2  680  pm2.621  701  orim1d  736  orim2d  737  pm2.63  749  pm2.74  756  simprimdc  794  oplem1  921  equsex  1663  equsexd  1664  r19.36av  2518  r19.44av  2526  r19.45av  2527  reuss  3280  opthpr  3616  relop  4586  swoord2  6322  indpi  6901  lelttr  7573  elnnz  8760  ztri3or0  8792  xrlelttr  9271  icossicc  9378  iocssicc  9379  ioossico  9380  bj-exlimmp  11670