Theorem sklem 230

Description: Soundness lemma.

Hypothesis

Ref	Expression
sklem.1	a =< b

Assertion

Ref	Expression
sklem	(a' v b) = 1

Proof of Theorem sklem

Step	Hyp	Ref	Expression
1		or12 80	. . 3 (a' v (a v b)) = (a v (a' v b))
2		df-t 41	. . . . . 6 1 = (a v a')
3	2	ax-r5 38	. . . . 5 (1 v b) = ((a v a') v b)
4	3	ax-r1 35	. . . 4 ((a v a') v b) = (1 v b)
5		ax-a3 32	. . . 4 ((a v a') v b) = (a v (a' v b))
6		ax-a2 31	. . . 4 (1 v b) = (b v 1)
7	4, 5, 6	3tr2 64	. . 3 (a v (a' v b)) = (b v 1)
8	1, 7	ax-r2 36	. 2 (a' v (a v b)) = (b v 1)
9		sklem.1	. . . 4 a =< b
10	9	df-le2 131	. . 3 (a v b) = b
11	10	lor 70	. 2 (a' v (a v b)) = (a' v b)
12		or1 104	. 2 (b v 1) = 1
13	8, 11, 12	3tr2 64	1 (a' v b) = 1

Syntax hints:   = wb 1   =< wle 2  'wn 4   v wo 6  1wt 8

This theorem is referenced by:  ska13 241  ska15 244  lei3 246  oaidlem1 294  id5id0 352  u1lemle1 710  u2lemle1 711  u3lemle1 712  u4lemle1 713  u5lemle1 714  lem3.3.3 1051  lem3.3.7i4e1 1068  lem3.3.7i4e2 1069  lem4.6.7 1100

This theorem was proved from axioms:  ax-a2 31  ax-a3 32  ax-a4 33  ax-r1 35  ax-r2 36  ax-r5 38

This theorem depends on definitions:  df-t 41  df-le2 131

Copyright terms: Public domain