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  69  ancld  308  ancrd  309  anim12d  318  anim1d  319  anim2d  320  orel2  644  pm2.621  665  orim1d  700  orim2d  701  pm2.63  712  pm2.74  719  simprimdc  755  oplem1  881  equsex  1613  equsexd  1614  r19.36av  2455  r19.44av  2463  r19.45av  2464  eqsbc3r  2813  reuss  3212  opthpr  3534  relop  4429  swoord2  6072  indpi  6326  lelttr  6903  elnnz  8031  ztri3or0  8063  xrlelttr  8492  icossicc  8599  iocssicc  8600  ioossico  8601  bj-exlimmp  9244