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

---

Theorem orval 137

Description: Value of the disjunction.

Hypotheses

Ref	Expression
imval.1
imval.2

Assertion

Ref	Expression
orval

Distinct variable groups:   ,   ,

---

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

Step	Hyp	Ref	Expression
1		wor 130	. . 3
2		imval.1	. . 3
3		imval.2	. . 3
4	1, 2, 3	wov 64	. 2
5		df-or 122	. . 3
6	1, 2, 3, 5	oveq 92	. 2
7		wal 124	. . . 4
8		wim 127	. . . . . 6
9		wv 58	. . . . . . 7
10		wv 58	. . . . . . 7
11	8, 9, 10	wov 64	. . . . . 6
12		wv 58	. . . . . . . 8
13	8, 12, 10	wov 64	. . . . . . 7
14	8, 13, 10	wov 64	. . . . . 6
15	8, 11, 14	wov 64	. . . . 5
16	15	wl 59	. . . 4
17	7, 16	wc 45	. . 3
18	9, 2	weqi 68	. . . . . . . 8
19	18	id 25	. . . . . . 7
20	8, 9, 10, 19	oveq1 89	. . . . . 6
21	8, 11, 14, 20	oveq1 89	. . . . 5
22	15, 21	leq 81	. . . 4
23	7, 16, 22	ceq2 80	. . 3
24	8, 2, 10	wov 64	. . . . . 6
25	8, 24, 14	wov 64	. . . . 5
26	25	wl 59	. . . 4
27	12, 3	weqi 68	. . . . . . . . 9
28	27	id 25	. . . . . . . 8
29	8, 12, 10, 28	oveq1 89	. . . . . . 7
30	8, 13, 10, 29	oveq1 89	. . . . . 6
31	8, 24, 14, 30	oveq2 91	. . . . 5
32	25, 31	leq 81	. . . 4
33	7, 26, 32	ceq2 80	. . 3
34	17, 2, 3, 23, 33	ovl 107	. 2
35	4, 6, 34	eqtri 85	1

Colors of variables: type var term

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

This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-id 24  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-refl 39  ax-eqmp 42  ax-ceq 46  ax-beta 60  ax-distrc 61  ax-leq 62  ax-distrl 63  ax-hbl1 93  ax-17 95  ax-inst 103

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

This theorem is referenced by:  ecase  153  olc  154  orc  155

Copyright terms: Public domain

W3C validator