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

---

Theorem exlimdv2 156

Description: Existential elimination.

Hypotheses

Ref	Expression
exlimdv2.1
exlimdv2.2

Assertion

Ref	Expression
exlimdv2

Distinct variable groups:   ,   ,   ,   ,

---

Proof of Theorem exlimdv2 Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		exlimdv2.2	. . 3
2	1	ax-cb2 30	. 2
3	1	ex 148	. . . 4
4	3	alrimiv 141	. . 3
5		wex 129	. . . 4
6		exlimdv2.1	. . . 4
7	5, 6	wc 45	. . 3
8	4, 7	adantr 50	. 2
9	1	ax-cb1 29	. . . . . 6
10	9	wctl 31	. . . . 5
11	10, 7	simpr 23	. . . 4
12	10, 7	wct 44	. . . . 5
13	6	exval 133	. . . . 5
14	12, 13	a1i 28	. . . 4
15	11, 14	mpbi 72	. . 3
16		wim 127	. . . . 5
17		wal 124	. . . . . 6
18		wv 58	. . . . . . . . 9
19	6, 18	wc 45	. . . . . . . 8
20		wv 58	. . . . . . . 8
21	16, 19, 20	wov 64	. . . . . . 7
22	21	wl 59	. . . . . 6
23	17, 22	wc 45	. . . . 5
24	16, 23, 20	wov 64	. . . 4
25	20, 2	weqi 68	. . . . . . . . 9
26	25	id 25	. . . . . . . 8
27	16, 19, 20, 26	oveq2 91	. . . . . . 7
28	21, 27	leq 81	. . . . . 6
29	17, 22, 28	ceq2 80	. . . . 5
30	16, 23, 20, 29, 26	oveq12 90	. . . 4
31	24, 2, 30	cla4v 142	. . 3
32	15, 31	syl 16	. 2
33	2, 8, 32	mpd 146	1

Colors of variables: type var term

Syntax hints:  tv 1   ht 2  hb 3  kc 5  kl 6   ke 7  kbr 9  kct 10   wffMMJ2 11  wffMMJ2t 12   tim 111  tal 112  tex 113

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-ded 43  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-ex 121

This theorem is referenced by:  exlimdv  157  dfex2  185

Copyright terms: Public domain

W3C validator