Quantum Logic Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa3-1to5		Unicode version

---

Theorem oa3-1to5 993

Description: Derivation of an equivalent of the second "universal" 3-OA U2 from an equivalent of the first "universal" 3-OA U1. This shows that U2 is redundant in a system containg U1. The hypothesis is theorem oal1 1000.

Hypothesis

Ref	Expression
oa3-1to5.1

Assertion

Ref	Expression
oa3-1to5

---

Proof of Theorem oa3-1to5

Step	Hyp	Ref	Expression
1		leid 148	. . . . 5
2		oa3-1to5.1	. . . . 5
3	1, 2	lel2or 170	. . . 4
4	3	lelan 167	. . 3
5		ax-a1 30	. . . . . . . 8
6	5	ran 78	. . . . . . 7
7	6	ax-r5 38	. . . . . 6
8		ax-a2 31	. . . . . 6
9	7, 8	ax-r2 36	. . . . 5
10		u1lemab 610	. . . . 5
11		u1lemab 610	. . . . 5
12	9, 10, 11	3tr1 63	. . . 4
13		ancom 74	. . . 4
14		ancom 74	. . . 4
15	12, 13, 14	3tr1 63	. . 3
16	4, 15	lbtr 139	. 2
17		lear 161	. 2
18	16, 17	letr 137	1

Colors of variables: term

Syntax hints:   wle 2  wn 4   wo 6   wa 7   wi1 12

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator