Theorem ska3 224

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

Assertion

Ref	Expression
ska3	((a == b)_|_ v (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_|_) v (a == b)_|_) = ((a_|_ == b_|_) v (a_|_ == b_|_)_|_)
4		ax-a2 30	. 2 ((a == b)_|_ v (a_|_ == b_|_)) = ((a_|_ == b_|_) v (a == b)_|_)
5		df-t 40	. 2 1 = ((a_|_ == b_|_) v (a_|_ == b_|_)_|_)
6	3, 4, 5	3tr1 60	1 ((a == b)_|_ v (a_|_ == b_|_)) = 1

Syntax hints:   = wb 1  _|_wn 4   == tb 5   v 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