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

---

Theorem comanblem2 871

Description: Lemma for biconditional commutation law.

Assertion

Ref	Expression
comanblem2

---

Proof of Theorem comanblem2

Step	Hyp	Ref	Expression
1		dfb 94	. . . 4
2		dfb 94	. . . 4
3	1, 2	2an 79	. . 3
4	3	lan 77	. 2
5		comanr1 464	. . . . . 6
6		comanr1 464	. . . . . . 7
7	6	comcom6 459	. . . . . 6
8	5, 7	fh1 469	. . . . 5
9		anass 76	. . . . . . . 8
10	9	ax-r1 35	. . . . . . 7
11		anidm 111	. . . . . . . 8
12	11	ran 78	. . . . . . 7
13	10, 12	ax-r2 36	. . . . . 6
14		dff 101	. . . . . . . . 9
15	14	ran 78	. . . . . . . 8
16	15	ax-r1 35	. . . . . . 7
17		anass 76	. . . . . . 7
18		an0r 109	. . . . . . 7
19	16, 17, 18	3tr2 64	. . . . . 6
20	13, 19	2or 72	. . . . 5
21		or0 102	. . . . 5
22	8, 20, 21	3tr 65	. . . 4
23		comanr1 464	. . . . . 6
24		comanr1 464	. . . . . . 7
25	24	comcom6 459	. . . . . 6
26	23, 25	fh1 469	. . . . 5
27		anass 76	. . . . . . . 8
28	27	ax-r1 35	. . . . . . 7
29		anidm 111	. . . . . . . 8
30	29	ran 78	. . . . . . 7
31	28, 30	ax-r2 36	. . . . . 6
32		dff 101	. . . . . . . . 9
33	32	ran 78	. . . . . . . 8
34	33	ax-r1 35	. . . . . . 7
35		anass 76	. . . . . . 7
36	34, 35, 18	3tr2 64	. . . . . 6
37	31, 36	2or 72	. . . . 5
38		or0 102	. . . . 5
39	26, 37, 38	3tr 65	. . . 4
40	22, 39	2an 79	. . 3
41		an4 86	. . 3
42		anandir 115	. . 3
43	40, 41, 42	3tr1 63	. 2
44	4, 43	ax-r2 36	1

Colors of variables: term

Syntax hints:   wb 1  wn 4   tb 5   wo 6   wa 7  wf 9

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-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  comanb  872

Copyright terms: Public domain

W3C validator