Theorem u4lemoa 623

Description: Lemma for non-tollens implication study. (Contributed by NM, 15-Dec-1997.)

Assertion

Ref	Expression
u4lemoa	((a →4 b) ∪ a) = 1

Proof of Theorem u4lemoa

Step	Hyp	Ref	Expression
1		df-i4 47	. . 3 (a →4 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ ))
2	1	ax-r5 38	. 2 ((a →4 b) ∪ a) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ )) ∪ a)
3		ax-a3 32	. . 3 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ )) ∪ a) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (((a⊥ ∪ b) ∩ b⊥ ) ∪ a))
4		comor1 461	. . . . . . . 8 (a⊥ ∪ b) C a⊥
5	4	comcom7 460	. . . . . . 7 (a⊥ ∪ b) C a
6		comor2 462	. . . . . . . 8 (a⊥ ∪ b) C b
7	6	comcom2 183	. . . . . . 7 (a⊥ ∪ b) C b⊥
8	5, 7	fh4r 476	. . . . . 6 (((a⊥ ∪ b) ∩ b⊥ ) ∪ a) = (((a⊥ ∪ b) ∪ a) ∩ (b⊥ ∪ a))
9		or32 82	. . . . . . . . 9 ((a⊥ ∪ b) ∪ a) = ((a⊥ ∪ a) ∪ b)
10		ax-a2 31	. . . . . . . . . 10 ((a⊥ ∪ a) ∪ b) = (b ∪ (a⊥ ∪ a))
11		df-t 41	. . . . . . . . . . . . . 14 1 = (a ∪ a⊥ )
12		ax-a2 31	. . . . . . . . . . . . . 14 (a ∪ a⊥ ) = (a⊥ ∪ a)
13	11, 12	ax-r2 36	. . . . . . . . . . . . 13 1 = (a⊥ ∪ a)
14	13	lor 70	. . . . . . . . . . . 12 (b ∪ 1) = (b ∪ (a⊥ ∪ a))
15	14	ax-r1 35	. . . . . . . . . . 11 (b ∪ (a⊥ ∪ a)) = (b ∪ 1)
16		or1 104	. . . . . . . . . . 11 (b ∪ 1) = 1
17	15, 16	ax-r2 36	. . . . . . . . . 10 (b ∪ (a⊥ ∪ a)) = 1
18	10, 17	ax-r2 36	. . . . . . . . 9 ((a⊥ ∪ a) ∪ b) = 1
19	9, 18	ax-r2 36	. . . . . . . 8 ((a⊥ ∪ b) ∪ a) = 1
20	19	ran 78	. . . . . . 7 (((a⊥ ∪ b) ∪ a) ∩ (b⊥ ∪ a)) = (1 ∩ (b⊥ ∪ a))
21		ancom 74	. . . . . . . 8 (1 ∩ (b⊥ ∪ a)) = ((b⊥ ∪ a) ∩ 1)
22		an1 106	. . . . . . . 8 ((b⊥ ∪ a) ∩ 1) = (b⊥ ∪ a)
23	21, 22	ax-r2 36	. . . . . . 7 (1 ∩ (b⊥ ∪ a)) = (b⊥ ∪ a)
24	20, 23	ax-r2 36	. . . . . 6 (((a⊥ ∪ b) ∪ a) ∩ (b⊥ ∪ a)) = (b⊥ ∪ a)
25	8, 24	ax-r2 36	. . . . 5 (((a⊥ ∪ b) ∩ b⊥ ) ∪ a) = (b⊥ ∪ a)
26	25	lor 70	. . . 4 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (((a⊥ ∪ b) ∩ b⊥ ) ∪ a)) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (b⊥ ∪ a))
27		ax-a3 32	. . . . 5 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (b⊥ ∪ a)) = ((a ∩ b) ∪ ((a⊥ ∩ b) ∪ (b⊥ ∪ a)))
28		ax-a2 31	. . . . . . . 8 ((a⊥ ∩ b) ∪ (b⊥ ∪ a)) = ((b⊥ ∪ a) ∪ (a⊥ ∩ b))
29		ancom 74	. . . . . . . . . . 11 (a⊥ ∩ b) = (b ∩ a⊥ )
30		anor1 88	. . . . . . . . . . 11 (b ∩ a⊥ ) = (b⊥ ∪ a)⊥
31	29, 30	ax-r2 36	. . . . . . . . . 10 (a⊥ ∩ b) = (b⊥ ∪ a)⊥
32	31	lor 70	. . . . . . . . 9 ((b⊥ ∪ a) ∪ (a⊥ ∩ b)) = ((b⊥ ∪ a) ∪ (b⊥ ∪ a)⊥ )
33		df-t 41	. . . . . . . . . 10 1 = ((b⊥ ∪ a) ∪ (b⊥ ∪ a)⊥ )
34	33	ax-r1 35	. . . . . . . . 9 ((b⊥ ∪ a) ∪ (b⊥ ∪ a)⊥ ) = 1
35	32, 34	ax-r2 36	. . . . . . . 8 ((b⊥ ∪ a) ∪ (a⊥ ∩ b)) = 1
36	28, 35	ax-r2 36	. . . . . . 7 ((a⊥ ∩ b) ∪ (b⊥ ∪ a)) = 1
37	36	lor 70	. . . . . 6 ((a ∩ b) ∪ ((a⊥ ∩ b) ∪ (b⊥ ∪ a))) = ((a ∩ b) ∪ 1)
38		or1 104	. . . . . 6 ((a ∩ b) ∪ 1) = 1
39	37, 38	ax-r2 36	. . . . 5 ((a ∩ b) ∪ ((a⊥ ∩ b) ∪ (b⊥ ∪ a))) = 1
40	27, 39	ax-r2 36	. . . 4 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (b⊥ ∪ a)) = 1
41	26, 40	ax-r2 36	. . 3 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (((a⊥ ∪ b) ∩ b⊥ ) ∪ a)) = 1
42	3, 41	ax-r2 36	. 2 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ )) ∪ a) = 1
43	2, 42	ax-r2 36	1 ((a →4 b) ∪ a) = 1

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →₄ wi4 15

This proof depends on 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 proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i4 47  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by:  u4lemnana  648