Higher-Order Logic Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  dedi		Unicode version

---

Theorem dedi 75

Description: Deduction theorem for equality.

Hypotheses

Ref	Expression
dedi.1
dedi.2

Assertion

Ref	Expression
dedi

---

Proof of Theorem dedi

Step	Hyp	Ref	Expression
1		dedi.1	. . 3
2		wtru 40	. . 3
3	1, 2	adantl 51	. 2
4		dedi.2	. . 3
5	4, 2	adantl 51	. 2
6	3, 5	ded 74	1

Colors of variables: type var term

Syntax hints:   ke 7  kt 8  kbr 9   wffMMJ2 11

This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-refl 39  ax-eqmp 42  ax-ded 43  ax-ceq 46

This theorem depends on definitions:  df-ov 65

This theorem is referenced by:  dfan2  144  notval2  149  alnex  174  notnot  187

Copyright terms: Public domain

W3C validator