Theorem ska3 232

Description: Soundness theorem for Kalmbach's quantum propositional logic axiom KA3. (Contributed by NM, 30-Aug-1997.)

Assertion

Ref	Expression
ska3	((a ≡ b)⊥ ∪ (a⊥ ≡ b⊥ )) = 1

Proof of Theorem ska3

Step	Hyp	Ref	Expression
1		conb 122	. . . 4 (a ≡ b) = (a⊥ ≡ b⊥ )
2	1	ax-r4 37	. . 3 (a ≡ b)⊥ = (a⊥ ≡ b⊥ )⊥
3	2	lor 70	. 2 ((a⊥ ≡ b⊥ ) ∪ (a ≡ b)⊥ ) = ((a⊥ ≡ b⊥ ) ∪ (a⊥ ≡ b⊥ )⊥ )
4		ax-a2 31	. 2 ((a ≡ b)⊥ ∪ (a⊥ ≡ b⊥ )) = ((a⊥ ≡ b⊥ ) ∪ (a ≡ b)⊥ )
5		df-t 41	. 2 1 = ((a⊥ ≡ b⊥ ) ∪ (a⊥ ≡ b⊥ )⊥ )
6	3, 4, 5	3tr1 63	1 ((a ≡ b)⊥ ∪ (a⊥ ≡ b⊥ )) = 1

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6  1wt 8

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This proof depends on definitions:  df-b 39  df-a 40  df-t 41

This theorem is used by: (None)