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

---

Theorem ax5 194

Description: Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105.

Hypotheses

Ref	Expression
ax5.1
ax5.2

Assertion

Ref	Expression
ax5

Distinct variable group:   ,

---

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

Step	Hyp	Ref	Expression
1		ax5.2	. . . . . 6
2		ax5.1	. . . . . . . 8
3	2	ax4 140	. . . . . . 7
4		wal 124	. . . . . . . 8
5		wim 127	. . . . . . . . . 10
6	5, 2, 1	wov 64	. . . . . . . . 9
7	6	wl 59	. . . . . . . 8
8	4, 7	wc 45	. . . . . . 7
9	3, 8	adantl 51	. . . . . 6
10	6	ax4 140	. . . . . . 7
11	3	ax-cb1 29	. . . . . . 7
12	10, 11	adantr 50	. . . . . 6
13	1, 9, 12	mpd 146	. . . . 5
14		wv 58	. . . . . 6
15	4, 14	ax-17 95	. . . . . . 7
16	6, 14	ax-hbl1 93	. . . . . . 7
17	4, 7, 14, 15, 16	hbc 100	. . . . . 6
18	2	wl 59	. . . . . . 7
19	2, 14	ax-hbl1 93	. . . . . . 7
20	4, 18, 14, 15, 19	hbc 100	. . . . . 6
21	8, 14, 11, 17, 20	hbct 145	. . . . 5
22	13, 21	alrimi 170	. . . 4
23	22	ex 148	. . 3
24		wtru 40	. . 3
25	23, 24	adantl 51	. 2
26	25	ex 148	1

Colors of variables: type var term

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

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  ax-eta 165

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

This theorem is referenced by:  ax11  201

Copyright terms: Public domain

W3C validator