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

Theorem i3con 551
Description: Theorem for Kalmbach implication. (Contributed by NM, 9-Nov-1997.)
Assertion
Ref Expression
i3con ((a3 b) →3 ((a3 b) →3 (b3 a ))) = 1

Proof of Theorem i3con
StepHypRef Expression
1 ni32 502 . . . . 5 (a3 b) = ((ab) ∩ ((ab ) ∪ (a ∩ (ab ))))
2 i3n1 249 . . . . 5 (b3 a ) = (((ba ) ∪ (ba)) ∪ (b ∩ (ba )))
31, 22or 72 . . . 4 ((a3 b) ∪ (b3 a )) = (((ab) ∩ ((ab ) ∪ (a ∩ (ab )))) ∪ (((ba ) ∪ (ba)) ∪ (b ∩ (ba ))))
4 ax-a2 31 . . . . 5 (((ab) ∩ ((ab ) ∪ (a ∩ (ab )))) ∪ (((ba ) ∪ (ba)) ∪ (b ∩ (ba )))) = ((((ba ) ∪ (ba)) ∪ (b ∩ (ba ))) ∪ ((ab) ∩ ((ab ) ∪ (a ∩ (ab )))))
5 comor2 462 . . . . . . . . . 10 (ab) C b
6 comor1 461 . . . . . . . . . . 11 (ab) C a
76comcom2 183 . . . . . . . . . 10 (ab) C a
85, 7com2an 484 . . . . . . . . 9 (ab) C (ba )
95, 6com2an 484 . . . . . . . . 9 (ab) C (ba)
108, 9com2or 483 . . . . . . . 8 (ab) C ((ba ) ∪ (ba))
115comcom2 183 . . . . . . . . 9 (ab) C b
125, 7com2or 483 . . . . . . . . 9 (ab) C (ba )
1311, 12com2an 484 . . . . . . . 8 (ab) C (b ∩ (ba ))
1410, 13com2or 483 . . . . . . 7 (ab) C (((ba ) ∪ (ba)) ∪ (b ∩ (ba )))
156, 11com2an 484 . . . . . . . 8 (ab) C (ab )
166, 11com2or 483 . . . . . . . . 9 (ab) C (ab )
177, 16com2an 484 . . . . . . . 8 (ab) C (a ∩ (ab ))
1815, 17com2or 483 . . . . . . 7 (ab) C ((ab ) ∪ (a ∩ (ab )))
1914, 18fh4 472 . . . . . 6 ((((ba ) ∪ (ba)) ∪ (b ∩ (ba ))) ∪ ((ab) ∩ ((ab ) ∪ (a ∩ (ab ))))) = (((((ba ) ∪ (ba)) ∪ (b ∩ (ba ))) ∪ (ab)) ∩ ((((ba ) ∪ (ba)) ∪ (b ∩ (ba ))) ∪ ((ab ) ∪ (a ∩ (ab )))))
20 ax-a3 32 . . . . . . . 8 ((((ba ) ∪ (ba)) ∪ (b ∩ (ba ))) ∪ (ab)) = (((ba ) ∪ (ba)) ∪ ((b ∩ (ba )) ∪ (ab)))
21 or12 80 . . . . . . . . 9 (((ba ) ∪ (ba)) ∪ ((b ∩ (ba )) ∪ (ab))) = ((b ∩ (ba )) ∪ (((ba ) ∪ (ba)) ∪ (ab)))
22 ax-a3 32 . . . . . . . . . . . 12 (((ba ) ∪ (ba)) ∪ (ab)) = ((ba ) ∪ ((ba) ∪ (ab)))
23 ancom 74 . . . . . . . . . . . . . . . . 17 (ba) = (ab)
24 lea 160 . . . . . . . . . . . . . . . . 17 (ab) ≤ a
2523, 24bltr 138 . . . . . . . . . . . . . . . 16 (ba) ≤ a
26 leo 158 . . . . . . . . . . . . . . . 16 a ≤ (ab)
2725, 26letr 137 . . . . . . . . . . . . . . 15 (ba) ≤ (ab)
2827df-le2 131 . . . . . . . . . . . . . 14 ((ba) ∪ (ab)) = (ab)
2928lor 70 . . . . . . . . . . . . 13 ((ba ) ∪ ((ba) ∪ (ab))) = ((ba ) ∪ (ab))
30 ax-a2 31 . . . . . . . . . . . . . 14 ((ba ) ∪ (ab)) = ((ab) ∪ (ba ))
31 ax-a3 32 . . . . . . . . . . . . . . 15 ((ab) ∪ (ba )) = (a ∪ (b ∪ (ba )))
32 orabs 120 . . . . . . . . . . . . . . . 16 (b ∪ (ba )) = b
3332lor 70 . . . . . . . . . . . . . . 15 (a ∪ (b ∪ (ba ))) = (ab)
3431, 33ax-r2 36 . . . . . . . . . . . . . 14 ((ab) ∪ (ba )) = (ab)
3530, 34ax-r2 36 . . . . . . . . . . . . 13 ((ba ) ∪ (ab)) = (ab)
3629, 35ax-r2 36 . . . . . . . . . . . 12 ((ba ) ∪ ((ba) ∪ (ab))) = (ab)
3722, 36ax-r2 36 . . . . . . . . . . 11 (((ba ) ∪ (ba)) ∪ (ab)) = (ab)
3837lor 70 . . . . . . . . . 10 ((b ∩ (ba )) ∪ (((ba ) ∪ (ba)) ∪ (ab))) = ((b ∩ (ba )) ∪ (ab))
39 ax-a2 31 . . . . . . . . . . 11 ((b ∩ (ba )) ∪ (ab)) = ((ab) ∪ (b ∩ (ba )))
405comcom 453 . . . . . . . . . . . . . 14 b C (ab)
4140comcom3 454 . . . . . . . . . . . . 13 b C (ab)
42 comorr 184 . . . . . . . . . . . . . 14 b C (ba )
4342comcom3 454 . . . . . . . . . . . . 13 b C (ba )
4441, 43fh4 472 . . . . . . . . . . . 12 ((ab) ∪ (b ∩ (ba ))) = (((ab) ∪ b ) ∩ ((ab) ∪ (ba )))
45 ax-a3 32 . . . . . . . . . . . . . . 15 ((ab) ∪ b ) = (a ∪ (bb ))
46 df-t 41 . . . . . . . . . . . . . . . . . 18 1 = (bb )
4746ax-r1 35 . . . . . . . . . . . . . . . . 17 (bb ) = 1
4847lor 70 . . . . . . . . . . . . . . . 16 (a ∪ (bb )) = (a ∪ 1)
49 or1 104 . . . . . . . . . . . . . . . 16 (a ∪ 1) = 1
5048, 49ax-r2 36 . . . . . . . . . . . . . . 15 (a ∪ (bb )) = 1
5145, 50ax-r2 36 . . . . . . . . . . . . . 14 ((ab) ∪ b ) = 1
52 ax-a2 31 . . . . . . . . . . . . . . . 16 (ab) = (ba)
5352ax-r5 38 . . . . . . . . . . . . . . 15 ((ab) ∪ (ba )) = ((ba) ∪ (ba ))
54 or4 84 . . . . . . . . . . . . . . . 16 ((ba) ∪ (ba )) = ((bb) ∪ (aa ))
55 df-t 41 . . . . . . . . . . . . . . . . . . 19 1 = (aa )
5655ax-r1 35 . . . . . . . . . . . . . . . . . 18 (aa ) = 1
5756lor 70 . . . . . . . . . . . . . . . . 17 ((bb) ∪ (aa )) = ((bb) ∪ 1)
58 or1 104 . . . . . . . . . . . . . . . . 17 ((bb) ∪ 1) = 1
5957, 58ax-r2 36 . . . . . . . . . . . . . . . 16 ((bb) ∪ (aa )) = 1
6054, 59ax-r2 36 . . . . . . . . . . . . . . 15 ((ba) ∪ (ba )) = 1
6153, 60ax-r2 36 . . . . . . . . . . . . . 14 ((ab) ∪ (ba )) = 1
6251, 612an 79 . . . . . . . . . . . . 13 (((ab) ∪ b ) ∩ ((ab) ∪ (ba ))) = (1 ∩ 1)
63 an1 106 . . . . . . . . . . . . 13 (1 ∩ 1) = 1
6462, 63ax-r2 36 . . . . . . . . . . . 12 (((ab) ∪ b ) ∩ ((ab) ∪ (ba ))) = 1
6544, 64ax-r2 36 . . . . . . . . . . 11 ((ab) ∪ (b ∩ (ba ))) = 1
6639, 65ax-r2 36 . . . . . . . . . 10 ((b ∩ (ba )) ∪ (ab)) = 1
6738, 66ax-r2 36 . . . . . . . . 9 ((b ∩ (ba )) ∪ (((ba ) ∪ (ba)) ∪ (ab))) = 1
6821, 67ax-r2 36 . . . . . . . 8 (((ba ) ∪ (ba)) ∪ ((b ∩ (ba )) ∪ (ab))) = 1
6920, 68ax-r2 36 . . . . . . 7 ((((ba ) ∪ (ba)) ∪ (b ∩ (ba ))) ∪ (ab)) = 1
70 ax-a3 32 . . . . . . . 8 ((((ba ) ∪ (ba)) ∪ (b ∩ (ba ))) ∪ ((ab ) ∪ (a ∩ (ab )))) = (((ba ) ∪ (ba)) ∪ ((b ∩ (ba )) ∪ ((ab ) ∪ (a ∩ (ab )))))
71 ax-a2 31 . . . . . . . . . . 11 ((ba ) ∪ (ba)) = ((ba) ∪ (ba ))
72 ancom 74 . . . . . . . . . . . 12 (ba ) = (ab)
7372lor 70 . . . . . . . . . . 11 ((ba) ∪ (ba )) = ((ba) ∪ (ab))
7471, 73ax-r2 36 . . . . . . . . . 10 ((ba ) ∪ (ba)) = ((ba) ∪ (ab))
75 ax-a3 32 . . . . . . . . . . . 12 (((b ∩ (ba )) ∪ (ab )) ∪ (a ∩ (ab ))) = ((b ∩ (ba )) ∪ ((ab ) ∪ (a ∩ (ab ))))
7675ax-r1 35 . . . . . . . . . . 11 ((b ∩ (ba )) ∪ ((ab ) ∪ (a ∩ (ab )))) = (((b ∩ (ba )) ∪ (ab )) ∪ (a ∩ (ab )))
77 ax-a2 31 . . . . . . . . . . . . 13 ((b ∩ (ba )) ∪ (ab )) = ((ab ) ∪ (b ∩ (ba )))
78 coman2 186 . . . . . . . . . . . . . . . 16 (ab ) C b
7978comcom 453 . . . . . . . . . . . . . . 15 b C (ab )
8079, 43fh4 472 . . . . . . . . . . . . . 14 ((ab ) ∪ (b ∩ (ba ))) = (((ab ) ∪ b ) ∩ ((ab ) ∪ (ba )))
81 ax-a2 31 . . . . . . . . . . . . . . . . 17 ((ab ) ∪ b ) = (b ∪ (ab ))
82 ancom 74 . . . . . . . . . . . . . . . . . . 19 (ab ) = (ba)
8382lor 70 . . . . . . . . . . . . . . . . . 18 (b ∪ (ab )) = (b ∪ (ba))
84 orabs 120 . . . . . . . . . . . . . . . . . 18 (b ∪ (ba)) = b
8583, 84ax-r2 36 . . . . . . . . . . . . . . . . 17 (b ∪ (ab )) = b
8681, 85ax-r2 36 . . . . . . . . . . . . . . . 16 ((ab ) ∪ b ) = b
87 ax-a2 31 . . . . . . . . . . . . . . . . . . 19 (ba ) = (ab)
88 anor1 88 . . . . . . . . . . . . . . . . . . . . 21 (ab ) = (ab)
8988con2 67 . . . . . . . . . . . . . . . . . . . 20 (ab ) = (ab)
9089ax-r1 35 . . . . . . . . . . . . . . . . . . 19 (ab) = (ab )
9187, 90ax-r2 36 . . . . . . . . . . . . . . . . . 18 (ba ) = (ab )
9291lor 70 . . . . . . . . . . . . . . . . 17 ((ab ) ∪ (ba )) = ((ab ) ∪ (ab ) )
93 df-t 41 . . . . . . . . . . . . . . . . . 18 1 = ((ab ) ∪ (ab ) )
9493ax-r1 35 . . . . . . . . . . . . . . . . 17 ((ab ) ∪ (ab ) ) = 1
9592, 94ax-r2 36 . . . . . . . . . . . . . . . 16 ((ab ) ∪ (ba )) = 1
9686, 952an 79 . . . . . . . . . . . . . . 15 (((ab ) ∪ b ) ∩ ((ab ) ∪ (ba ))) = (b ∩ 1)
97 an1 106 . . . . . . . . . . . . . . 15 (b ∩ 1) = b
9896, 97ax-r2 36 . . . . . . . . . . . . . 14 (((ab ) ∪ b ) ∩ ((ab ) ∪ (ba ))) = b
9980, 98ax-r2 36 . . . . . . . . . . . . 13 ((ab ) ∪ (b ∩ (ba ))) = b
10077, 99ax-r2 36 . . . . . . . . . . . 12 ((b ∩ (ba )) ∪ (ab )) = b
101100ax-r5 38 . . . . . . . . . . 11 (((b ∩ (ba )) ∪ (ab )) ∪ (a ∩ (ab ))) = (b ∪ (a ∩ (ab )))
10276, 101ax-r2 36 . . . . . . . . . 10 ((b ∩ (ba )) ∪ ((ab ) ∪ (a ∩ (ab )))) = (b ∪ (a ∩ (ab )))
10374, 1022or 72 . . . . . . . . 9 (((ba ) ∪ (ba)) ∪ ((b ∩ (ba )) ∪ ((ab ) ∪ (a ∩ (ab ))))) = (((ba) ∪ (ab)) ∪ (b ∪ (a ∩ (ab ))))
104 or4 84 . . . . . . . . . 10 (((ba) ∪ (ab)) ∪ (b ∪ (a ∩ (ab )))) = (((ba) ∪ b ) ∪ ((ab) ∪ (a ∩ (ab ))))
105 coman1 185 . . . . . . . . . . . . . . 15 (ab) C a
106105comcom 453 . . . . . . . . . . . . . 14 a C (ab)
107 comorr 184 . . . . . . . . . . . . . . 15 a C (ab )
108107comcom3 454 . . . . . . . . . . . . . 14 a C (ab )
109106, 108fh4 472 . . . . . . . . . . . . 13 ((ab) ∪ (a ∩ (ab ))) = (((ab) ∪ a ) ∩ ((ab) ∪ (ab )))
110 ax-a2 31 . . . . . . . . . . . . . . . 16 ((ab) ∪ a ) = (a ∪ (ab))
111 orabs 120 . . . . . . . . . . . . . . . 16 (a ∪ (ab)) = a
112110, 111ax-r2 36 . . . . . . . . . . . . . . 15 ((ab) ∪ a ) = a
113 anor2 89 . . . . . . . . . . . . . . . . . . 19 (ab) = (ab )
114113con2 67 . . . . . . . . . . . . . . . . . 18 (ab) = (ab )
115114ax-r1 35 . . . . . . . . . . . . . . . . 17 (ab ) = (ab)
116115lor 70 . . . . . . . . . . . . . . . 16 ((ab) ∪ (ab )) = ((ab) ∪ (ab) )
117 df-t 41 . . . . . . . . . . . . . . . . 17 1 = ((ab) ∪ (ab) )
118117ax-r1 35 . . . . . . . . . . . . . . . 16 ((ab) ∪ (ab) ) = 1
119116, 118ax-r2 36 . . . . . . . . . . . . . . 15 ((ab) ∪ (ab )) = 1
120112, 1192an 79 . . . . . . . . . . . . . 14 (((ab) ∪ a ) ∩ ((ab) ∪ (ab ))) = (a ∩ 1)
121 an1 106 . . . . . . . . . . . . . 14 (a ∩ 1) = a
122120, 121ax-r2 36 . . . . . . . . . . . . 13 (((ab) ∪ a ) ∩ ((ab) ∪ (ab ))) = a
123109, 122ax-r2 36 . . . . . . . . . . . 12 ((ab) ∪ (a ∩ (ab ))) = a
124123lor 70 . . . . . . . . . . 11 (((ba) ∪ b ) ∪ ((ab) ∪ (a ∩ (ab )))) = (((ba) ∪ b ) ∪ a )
125 df-a 40 . . . . . . . . . . . . . . 15 (ba) = (ba )
126125con2 67 . . . . . . . . . . . . . 14 (ba) = (ba )
127126ax-r1 35 . . . . . . . . . . . . 13 (ba ) = (ba)
128127lor 70 . . . . . . . . . . . 12 ((ba) ∪ (ba )) = ((ba) ∪ (ba) )
129 ax-a3 32 . . . . . . . . . . . 12 (((ba) ∪ b ) ∪ a ) = ((ba) ∪ (ba ))
130 df-t 41 . . . . . . . . . . . 12 1 = ((ba) ∪ (ba) )
131128, 129, 1303tr1 63 . . . . . . . . . . 11 (((ba) ∪ b ) ∪ a ) = 1
132124, 131ax-r2 36 . . . . . . . . . 10 (((ba) ∪ b ) ∪ ((ab) ∪ (a ∩ (ab )))) = 1
133104, 132ax-r2 36 . . . . . . . . 9 (((ba) ∪ (ab)) ∪ (b ∪ (a ∩ (ab )))) = 1
134103, 133ax-r2 36 . . . . . . . 8 (((ba ) ∪ (ba)) ∪ ((b ∩ (ba )) ∪ ((ab ) ∪ (a ∩ (ab ))))) = 1
13570, 134ax-r2 36 . . . . . . 7 ((((ba ) ∪ (ba)) ∪ (b ∩ (ba ))) ∪ ((ab ) ∪ (a ∩ (ab )))) = 1
13669, 1352an 79 . . . . . 6 (((((ba ) ∪ (ba)) ∪ (b ∩ (ba ))) ∪ (ab)) ∩ ((((ba ) ∪ (ba)) ∪ (b ∩ (ba ))) ∪ ((ab ) ∪ (a ∩ (ab ))))) = (1 ∩ 1)
13719, 136ax-r2 36 . . . . 5 ((((ba ) ∪ (ba)) ∪ (b ∩ (ba ))) ∪ ((ab) ∩ ((ab ) ∪ (a ∩ (ab ))))) = (1 ∩ 1)
1384, 137ax-r2 36 . . . 4 (((ab) ∩ ((ab ) ∪ (a ∩ (ab )))) ∪ (((ba ) ∪ (ba)) ∪ (b ∩ (ba )))) = (1 ∩ 1)
1393, 138ax-r2 36 . . 3 ((a3 b) ∪ (b3 a )) = (1 ∩ 1)
140139, 63ax-r2 36 . 2 ((a3 b) ∪ (b3 a )) = 1
141140i0i3 512 1 ((a3 b) →3 ((a3 b) →3 (b3 a ))) = 1
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  1wt 8  3 wi3 14
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-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator