Theorem lei3 246

Description: L.e. to Kalmbach implication.

Hypothesis

Ref	Expression
lei3.1	a =< b

Assertion

Ref	Expression
lei3	(a ->3 b) = 1

Proof of Theorem lei3

Step	Hyp	Ref	Expression
1		ax-a3 32	. . 3 (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b))) = ((a' ^ b) v ((a' ^ b') v (a ^ (a' v b))))
2		ax-a2 31	. . . . 5 (b' v a) = (a v b')
3		ancom 74	. . . . . . 7 (a' ^ b') = (b' ^ a')
4		lei3.1	. . . . . . . . 9 a =< b
5	4	lecon 154	. . . . . . . 8 b' =< a'
6	5	df2le2 136	. . . . . . 7 (b' ^ a') = b'
7	3, 6	ax-r2 36	. . . . . 6 (a' ^ b') = b'
8	4	sklem 230	. . . . . . . 8 (a' v b) = 1
9	8	lan 77	. . . . . . 7 (a ^ (a' v b)) = (a ^ 1)
10		an1 106	. . . . . . 7 (a ^ 1) = a
11	9, 10	ax-r2 36	. . . . . 6 (a ^ (a' v b)) = a
12	7, 11	2or 72	. . . . 5 ((a' ^ b') v (a ^ (a' v b))) = (b' v a)
13		anor2 89	. . . . . 6 (a' ^ b) = (a v b')'
14	13	con2 67	. . . . 5 (a' ^ b)' = (a v b')
15	2, 12, 14	3tr1 63	. . . 4 ((a' ^ b') v (a ^ (a' v b))) = (a' ^ b)'
16	15	lor 70	. . 3 ((a' ^ b) v ((a' ^ b') v (a ^ (a' v b)))) = ((a' ^ b) v (a' ^ b)')
17	1, 16	ax-r2 36	. 2 (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b))) = ((a' ^ b) v (a' ^ b)')
18		df-i3 46	. 2 (a ->3 b) = (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))
19		df-t 41	. 2 1 = ((a' ^ b) v (a' ^ b)')
20	17, 18, 19	3tr1 63	1 (a ->3 b) = 1

Syntax hints:   = wb 1   =< wle 2  'wn 4   v wo 6   ^ wa 7  1wt 8   ->3 wi3 14

This theorem is referenced by:  bina3 284  bina4 285  bina5 286  bii3 516  binr1 517  binr2 518  binr3 519  i3ri3 538  i3li3 539  i32i3 540  i3th5 547  i3th7 549  i3th8 550

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

This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-i3 46  df-le1 130  df-le2 131

Copyright terms: Public domain