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.43d 65  pm2.63 428  anim1d 559  anim2d 560  orim1d 565  orim2d 566  dedlema 761  r19.36av 1757  r19.44av 1763  r19.45av 1764  reuss 2272  opthpr 2481  relop 3270  abfii4 4544  rankxplim3 4694  elnnz 6100  expeq0t 6525  expord2t 6543  0top 7585  opni3 7818  lmfexlem1 7907  grpnnncan2 8043  va1cnlem 8292  ipsubdir 8452  minveceu 8527  hmphsyma 10451

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

Copyright terms: Public domain