Theorem 3vth6 809

Description: A 3-variable theorem. (Contributed by NM, 18-Oct-1998.)

Assertion

Ref	Expression
3vth6	((a →2 b)⊥ →2 (b ∪ c)) = (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))

Proof of Theorem 3vth6

Step	Hyp	Ref	Expression
1		oridm 110	. . 3 (((a →2 b)⊥ →2 (b ∪ c)) ∪ ((a →2 b)⊥ →2 (b ∪ c))) = ((a →2 b)⊥ →2 (b ∪ c))
2	1	ax-r1 35	. 2 ((a →2 b)⊥ →2 (b ∪ c)) = (((a →2 b)⊥ →2 (b ∪ c)) ∪ ((a →2 b)⊥ →2 (b ∪ c)))
3		3vth4 807	. . . 4 ((a →2 b)⊥ →2 (b ∪ c)) = ((a →2 c)⊥ →2 (b ∪ c))
4	3	lor 70	. . 3 (((a →2 b)⊥ →2 (b ∪ c)) ∪ ((a →2 b)⊥ →2 (b ∪ c))) = (((a →2 b)⊥ →2 (b ∪ c)) ∪ ((a →2 c)⊥ →2 (b ∪ c)))
5		3vth5 808	. . . . 5 ((a →2 b)⊥ →2 (b ∪ c)) = (c ∪ ((a →2 b) ∩ (c →2 b)))
6		ax-a2 31	. . . . . . 7 (b ∪ c) = (c ∪ b)
7	6	ud2lem0a 258	. . . . . 6 ((a →2 c)⊥ →2 (b ∪ c)) = ((a →2 c)⊥ →2 (c ∪ b))
8		3vth5 808	. . . . . 6 ((a →2 c)⊥ →2 (c ∪ b)) = (b ∪ ((a →2 c) ∩ (b →2 c)))
9	7, 8	ax-r2 36	. . . . 5 ((a →2 c)⊥ →2 (b ∪ c)) = (b ∪ ((a →2 c) ∩ (b →2 c)))
10	5, 9	2or 72	. . . 4 (((a →2 b)⊥ →2 (b ∪ c)) ∪ ((a →2 c)⊥ →2 (b ∪ c))) = ((c ∪ ((a →2 b) ∩ (c →2 b))) ∪ (b ∪ ((a →2 c) ∩ (b →2 c))))
11		or4 84	. . . . 5 ((c ∪ ((a →2 b) ∩ (c →2 b))) ∪ (b ∪ ((a →2 c) ∩ (b →2 c)))) = ((c ∪ b) ∪ (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c))))
12		ax-a2 31	. . . . . . 7 (c ∪ b) = (b ∪ c)
13	12	ax-r5 38	. . . . . 6 ((c ∪ b) ∪ (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))) = ((b ∪ c) ∪ (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c))))
14		or4 84	. . . . . . 7 ((b ∪ c) ∪ (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))) = ((b ∪ ((a →2 b) ∩ (c →2 b))) ∪ (c ∪ ((a →2 c) ∩ (b →2 c))))
15		leo 158	. . . . . . . . . . 11 b ≤ (b ∪ (a⊥ ∩ b⊥ ))
16		df-i2 45	. . . . . . . . . . . 12 (a →2 b) = (b ∪ (a⊥ ∩ b⊥ ))
17	16	ax-r1 35	. . . . . . . . . . 11 (b ∪ (a⊥ ∩ b⊥ )) = (a →2 b)
18	15, 17	lbtr 139	. . . . . . . . . 10 b ≤ (a →2 b)
19		leo 158	. . . . . . . . . . 11 b ≤ (b ∪ (c⊥ ∩ b⊥ ))
20		df-i2 45	. . . . . . . . . . . 12 (c →2 b) = (b ∪ (c⊥ ∩ b⊥ ))
21	20	ax-r1 35	. . . . . . . . . . 11 (b ∪ (c⊥ ∩ b⊥ )) = (c →2 b)
22	19, 21	lbtr 139	. . . . . . . . . 10 b ≤ (c →2 b)
23	18, 22	ler2an 173	. . . . . . . . 9 b ≤ ((a →2 b) ∩ (c →2 b))
24	23	df-le2 131	. . . . . . . 8 (b ∪ ((a →2 b) ∩ (c →2 b))) = ((a →2 b) ∩ (c →2 b))
25		leo 158	. . . . . . . . . . 11 c ≤ (c ∪ (a⊥ ∩ c⊥ ))
26		df-i2 45	. . . . . . . . . . . 12 (a →2 c) = (c ∪ (a⊥ ∩ c⊥ ))
27	26	ax-r1 35	. . . . . . . . . . 11 (c ∪ (a⊥ ∩ c⊥ )) = (a →2 c)
28	25, 27	lbtr 139	. . . . . . . . . 10 c ≤ (a →2 c)
29		leo 158	. . . . . . . . . . 11 c ≤ (c ∪ (b⊥ ∩ c⊥ ))
30		df-i2 45	. . . . . . . . . . . 12 (b →2 c) = (c ∪ (b⊥ ∩ c⊥ ))
31	30	ax-r1 35	. . . . . . . . . . 11 (c ∪ (b⊥ ∩ c⊥ )) = (b →2 c)
32	29, 31	lbtr 139	. . . . . . . . . 10 c ≤ (b →2 c)
33	28, 32	ler2an 173	. . . . . . . . 9 c ≤ ((a →2 c) ∩ (b →2 c))
34	33	df-le2 131	. . . . . . . 8 (c ∪ ((a →2 c) ∩ (b →2 c))) = ((a →2 c) ∩ (b →2 c))
35	24, 34	2or 72	. . . . . . 7 ((b ∪ ((a →2 b) ∩ (c →2 b))) ∪ (c ∪ ((a →2 c) ∩ (b →2 c)))) = (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))
36	14, 35	ax-r2 36	. . . . . 6 ((b ∪ c) ∪ (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))) = (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))
37	13, 36	ax-r2 36	. . . . 5 ((c ∪ b) ∪ (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))) = (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))
38	11, 37	ax-r2 36	. . . 4 ((c ∪ ((a →2 b) ∩ (c →2 b))) ∪ (b ∪ ((a →2 c) ∩ (b →2 c)))) = (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))
39	10, 38	ax-r2 36	. . 3 (((a →2 b)⊥ →2 (b ∪ c)) ∪ ((a →2 c)⊥ →2 (b ∪ c))) = (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))
40	4, 39	ax-r2 36	. 2 (((a →2 b)⊥ →2 (b ∪ c)) ∪ ((a →2 b)⊥ →2 (b ∪ c))) = (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))
41	2, 40	ax-r2 36	1 ((a →2 b)⊥ →2 (b ∪ c)) = (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   →₂ wi2 13

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

This theorem is used by:  3vth8  811