u1lem3var1 - Quantum Logic Explorer

	Quantum Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > QLE Home > Th. List > u1lem3var1		GIF version

Theorem u1lem3var1 731

Description: A 3-variable formula. (Contributed by Josiah Burroughs, 26-May-2004.)

**Assertion**
Ref	Expression
u1lem3var1	(((a →₁c) ∩ (b →₁c))^⊥ ∪ (((a →₁c)^⊥ →₁c) ∩ ((b →₁c)^⊥ →₁c))) = 1

**Proof of Theorem u1lem3var1**
Step	Hyp	Ref	Expression
1		ax-a2 31	. 2 (((a →₁c) ∩ (b →₁c))^⊥ ∪ ((a →₁c) ∩ (b →₁c))) = (((a →₁c) ∩ (b →₁c)) ∪ ((a →₁c) ∩ (b →₁c))^⊥ )
2		u1lemn1b 730	. . . . 5 (a →₁c) = ((a →₁c)^⊥ →₁c)
3		u1lemn1b 730	. . . . 5 (b →₁c) = ((b →₁c)^⊥ →₁c)
4	2, 3	2an 79	. . . 4 ((a →₁c) ∩ (b →₁c)) = (((a →₁c)^⊥ →₁c) ∩ ((b →₁c)^⊥ →₁c))
5	4	ax-r1 35	. . 3 (((a →₁c)^⊥ →₁c) ∩ ((b →₁c)^⊥ →₁c)) = ((a →₁c) ∩ (b →₁c))
6	5	lor 70	. 2 (((a →₁c) ∩ (b →₁c))^⊥ ∪ (((a →₁c)^⊥ →₁c) ∩ ((b →₁c)^⊥ →₁c))) = (((a →₁c) ∩ (b →₁c))^⊥ ∪ ((a →₁c) ∩ (b →₁c)))
7		df-t 41	. 2 1 = (((a →₁c) ∩ (b →₁c)) ∪ ((a →₁c) ∩ (b →₁c))^⊥ )
8	1, 6, 7	3tr1 63	1 (((a →₁c) ∩ (b →₁c))^⊥ ∪ (((a →₁c)^⊥ →₁c) ∩ ((b →₁c)^⊥ →₁c))) = 1

Colors of variables: term

Syntax hints: = wb 1 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 1wt 8 →₁wi1 12

This theorem was proved from 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 theorem depends on definitions: df-a 40 df-t 41 df-f 42 df-i1 44

This theorem is referenced by: (None)