Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem idd 61

Description: Principle of identity with antecedent.

Assertion

Ref	Expression
idd

---

Proof of Theorem idd

Step	Hyp	Ref	Expression
1		id 59	. 2
2	1	a1i 8	1

Colors of variables: wff set class

Syntax hints:   wi 3

This theorem is referenced by:  pm2.43d 65  pm2.63 428  anim1d 558  anim2d 559  orim1d 564  orim2d 565  dedlema 760  r19.36av 1752  r19.44av 1758  r19.45av 1759  reuss 2266  opthpr 2476  relop 3265  abfii4 4538  rankxplim3 4686  elnnz 6092  expeq0t 6517  expord2t 6535  0top 7577  opni3 7806  lmfexlem1 7891  grpnnncan2 8028  va1cnlem 8279  ipsubdir 8439  minveceu 8514  hmphsyma 10415

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

Copyright terms: Public domain