Theorem lem3.3.6 1056

Description: Equation 3.6 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)

Assertion

Ref	Expression
lem3.3.6	(a →2 (b ∪ c)) = ((a ∪ c) →2 (b ∪ c))

Proof of Theorem lem3.3.6

Step	Hyp	Ref	Expression
1		anor3 90	. . . . . 6 (b⊥ ∩ c⊥ ) = (b ∪ c)⊥
2	1	ax-r1 35	. . . . 5 (b ∪ c)⊥ = (b⊥ ∩ c⊥ )
3	2	lan 77	. . . 4 (a⊥ ∩ (b ∪ c)⊥ ) = (a⊥ ∩ (b⊥ ∩ c⊥ ))
4		anandir 115	. . . . 5 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) = ((a⊥ ∩ c⊥ ) ∩ (b⊥ ∩ c⊥ ))
5		anass 76	. . . . 5 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) = (a⊥ ∩ (b⊥ ∩ c⊥ ))
6		anor3 90	. . . . . 6 (a⊥ ∩ c⊥ ) = (a ∪ c)⊥
7	6, 1	2an 79	. . . . 5 ((a⊥ ∩ c⊥ ) ∩ (b⊥ ∩ c⊥ )) = ((a ∪ c)⊥ ∩ (b ∪ c)⊥ )
8	4, 5, 7	3tr2 64	. . . 4 (a⊥ ∩ (b⊥ ∩ c⊥ )) = ((a ∪ c)⊥ ∩ (b ∪ c)⊥ )
9	3, 8	ax-r2 36	. . 3 (a⊥ ∩ (b ∪ c)⊥ ) = ((a ∪ c)⊥ ∩ (b ∪ c)⊥ )
10	9	lor 70	. 2 ((b ∪ c) ∪ (a⊥ ∩ (b ∪ c)⊥ )) = ((b ∪ c) ∪ ((a ∪ c)⊥ ∩ (b ∪ c)⊥ ))
11		df-i2 45	. 2 (a →2 (b ∪ c)) = ((b ∪ c) ∪ (a⊥ ∩ (b ∪ c)⊥ ))
12		df-i2 45	. 2 ((a ∪ c) →2 (b ∪ c)) = ((b ∪ c) ∪ ((a ∪ c)⊥ ∩ (b ∪ c)⊥ ))
13	10, 11, 12	3tr1 63	1 (a →2 (b ∪ c)) = ((a ∪ c) →2 (b ∪ 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-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This proof depends on definitions:  df-a 40  df-t 41  df-f 42  df-i2 45

This theorem is used by:  lem3.4.6  1079