Theorem idd 61

Description: Principle of identity with antecedent.

Assertion

Ref	Expression
idd	|- (ph -> (ps -> ps))

Proof of Theorem idd

Step	Hyp	Ref	Expression
1		id 59	. 2 |- (ps -> ps)
2	1	a1i 8	1 |- (ph -> (ps -> ps))

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.63 429  anim1d 562  anim2d 563  orim1d 568  orim2d 569  dedlema 765  r19.36av 1798  r19.44av 1804  r19.45av 1805  reuss 2320  opthpr 2533  relop 3338  abfii4 4648  rankxplim3 4800  elnnz 6255  expeq0 6708  expord2 6726  0top 7759  opni3 7986  lmfexlem1 8076  grpnnncan2 8212  va1cnlem 8464  ipsubdir 8627  minveceu 8702  hmphsyma 10664

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain