wr5 - Quantum Logic Explorer

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

Theorem wr5 431

Description: Proof of weak orthomodular law from weaker-looking equivalent, wom3 367, which in turn is derived from ax-wom 361.

**Hypothesis**
Ref	Expression
wr5.1	(a ≡ b) = 1

**Assertion**
Ref	Expression
wr5	((a ∪ c) ≡ (b ∪ c)) = 1

**Proof of Theorem wr5**
Step	Hyp	Ref	Expression
1		wr5.1	. 2 (a ≡ b) = 1
2	1	wr5-2v 366	1 ((a ∪ c) ≡ (b ∪ c)) = 1

Colors of variables: term

Syntax hints: = wb 1 ≡ tb 5 ∪ wo 6 1wt 8

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

This theorem depends on definitions: df-b 39 df-a 40 df-t 41 df-f 42 df-i1 44 df-i2 45 df-le1 130 df-le2 131

This theorem is referenced by: wdka4o 1114