Theorem ska3 224

Description: Soundness theorem for Kalmbach's quantum propositional logic axiom KA3.

Assertion

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

Proof of Theorem ska3

Step	Hyp	Ref	Expression
1		conb 114	. . . 4 (a ≡ b) = (a⊥ ≡ b⊥ )
2	1	ax-r4 36	. . 3 (a ≡ b)⊥ = (a⊥ ≡ b⊥ )⊥
3	2	lor 66	. 2 ((a⊥ ≡ b⊥ ) ∪ (a ≡ b)⊥ ) = ((a⊥ ≡ b⊥ ) ∪ (a⊥ ≡ b⊥ )⊥ )
4		ax-a2 30	. 2 ((a ≡ b)⊥ ∪ (a⊥ ≡ b⊥ )) = ((a⊥ ≡ b⊥ ) ∪ (a ≡ b)⊥ )
5		df-t 40	. 2 1 = ((a⊥ ≡ b⊥ ) ∪ (a⊥ ≡ b⊥ )⊥ )
6	3, 4, 5	3tr1 60	1 ((a ≡ b)⊥ ∪ (a⊥ ≡ b⊥ )) = 1

Syntax hints:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6  1wt 9

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

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40

metamath.org