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 10	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  69  simprim  142  pm2.6  162  pm2.65  164  orel2  372  pm2.621  397  simpr  447  ancld  536  ancrd  537  anim12d  546  anim1d  547  anim2d  548  pm2.63  763  orim1d  812  orim2d  813  ecase2d  906  cad0  1400  merco2  1501  spnfw  1670  19.2OLD  1700  r19.36av  2760  r19.44av  2768  r19.45av  2769  eqsbc2  3104  reuss  3537  funiunfv  5468