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

---

Theorem wor 130

Description: Disjunction type.

Assertion

Ref	Expression
wor

---

Proof of Theorem wor Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wal 124	. . . . 5
2		wim 127	. . . . . . 7
3		wv 58	. . . . . . . 8
4		wv 58	. . . . . . . 8
5	2, 3, 4	wov 64	. . . . . . 7
6		wv 58	. . . . . . . . 9
7	2, 6, 4	wov 64	. . . . . . . 8
8	2, 7, 4	wov 64	. . . . . . 7
9	2, 5, 8	wov 64	. . . . . 6
10	9	wl 59	. . . . 5
11	1, 10	wc 45	. . . 4
12	11	wl 59	. . 3
13	12	wl 59	. 2
14		df-or 122	. 2
15	13, 14	eqtypri 71	1

Colors of variables: type var term

Syntax hints:  tv 1   ht 2  hb 3  kc 5  kl 6  kt 8  kbr 9  wffMMJ2t 12   tim 111  tal 112   tor 114

This theorem was proved from axioms:  ax-cb1 29  ax-refl 39

This theorem depends on definitions:  df-al 116  df-an 118  df-im 119  df-or 122

This theorem is referenced by:  orval  137  olc  154  orc  155  exmid  186

Copyright terms: Public domain

W3C validator