Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem u1lem3var1 713

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

**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 30	. 2 (((a →₁c) ∩ (b →₁c))^⊥ ∪ ((a →₁c) ∩ (b →₁c))) = (((a →₁c) ∩ (b →₁c)) ∪ ((a →₁c) ∩ (b →₁c))^⊥ )
2		u1lemn1b 712	. . . . 5 (a →₁c) = ((a →₁c)^⊥ →₁c)
3		u1lemn1b 712	. . . . 5 (b →₁c) = ((b →₁c)^⊥ →₁c)
4	2, 3	2an 72	. . . 4 ((a →₁c) ∩ (b →₁c)) = (((a →₁c)^⊥ →₁c) ∩ ((b →₁c)^⊥ →₁c))
5	4	ax-r1 34	. . 3 (((a →₁c)^⊥ →₁c) ∩ ((b →₁c)^⊥ →₁c)) = ((a →₁c) ∩ (b →₁c))
6	5	lor 66	. 2 (((a →₁c) ∩ (b →₁c))^⊥ ∪ (((a →₁c)^⊥ →₁c) ∩ ((b →₁c)^⊥ →₁c))) = (((a →₁c) ∩ (b →₁c))^⊥ ∪ ((a →₁c) ∩ (b →₁c)))
7		df-t 40	. 2 1 = (((a →₁c) ∩ (b →₁c)) ∪ ((a →₁c) ∩ (b →₁c))^⊥ )
8	1, 6, 7	3tr1 60	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 9 →₁wi1 13

This theorem was proved from axioms: ax-a1 29 ax-a2 30 ax-a3 31 ax-a5 33 ax-r1 34 ax-r2 35 ax-r4 36 ax-r5 37

This theorem depends on definitions: df-a 39 df-t 40 df-f 41 df-i1 43