Quantum Logic Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ax-arg		Unicode version

---

Axiom ax-arg 1151

Description: The Arguesian law as an axiom.

Hypothesis

Ref	Expression
arg.1	a0 b0 a1 b1 a2 b2

Assertion

Ref	Expression
ax-arg	a0 a1 b0 b1 a0 a2 b0 b2 a1 a2 b1 b2

---

Detailed syntax breakdown of Axiom ax-arg

Step	Hyp	Ref	Expression
1		wva0	. . . 4 a0
2		wva1	. . . 4 a1
3	1, 2	wo 6	. . 3 a0 a1
4		wvb0	. . . 4 b0
5		wvb1	. . . 4 b1
6	4, 5	wo 6	. . 3 b0 b1
7	3, 6	wa 7	. 2 a0 a1 b0 b1
8		wva2	. . . . 5 a2
9	1, 8	wo 6	. . . 4 a0 a2
10		wvb2	. . . . 5 b2
11	4, 10	wo 6	. . . 4 b0 b2
12	9, 11	wa 7	. . 3 a0 a2 b0 b2
13	2, 8	wo 6	. . . 4 a1 a2
14	5, 10	wo 6	. . . 4 b1 b2
15	13, 14	wa 7	. . 3 a1 a2 b1 b2
16	12, 15	wo 6	. 2 a0 a2 b0 b2 a1 a2 b1 b2
17	7, 16	wle 2	1 a0 a1 b0 b1 a0 a2 b0 b2 a1 a2 b1 b2

Colors of variables: term

This axiom is referenced by:  dp15lemb  1153  xdp15  1197  xxdp15  1200

Copyright terms: Public domain

W3C validator