Theorem eqidd 1513

Description: Class identity law with antecedent.

Assertion

Ref	Expression
eqidd	|- (ph -> A = A)

Proof of Theorem eqidd

Step	Hyp	Ref	Expression
1		eqid 1512	. 2 |- A = A
2	1	a1i 8	1 |- (ph -> A = A)

Syntax hints:   -> wi 3   = wceq 988

This theorem is referenced by:  1st2val 4175  2nd2val 4176  fsumconst 7161  climabs0i 7236  ser1f0i 7293  acdc3lem 7611  acdclem 7619  acdcALT 7621  minveclem9 8672  vri 10625  imonclem 10876  iepiclem 10886  cinvlem2 10891

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-ext 1494

This theorem depends on definitions:  df-bi 145  df-cleq 1505

Copyright terms: Public domain