Theorem oml 445

Description: Orthomodular law. Compare Th. 1 of Pavicic 1987.

Assertion

Ref	Expression
oml	(a v (a' ^ (a v b))) = (a v b)

Proof of Theorem oml

Step	Hyp	Ref	Expression
1		omlem1 127	. 2 ((a v (a' ^ (a v b))) v (a v b)) = (a v b)
2		omlem2 128	. 2 ((a v b)' v (a v (a' ^ (a v b)))) = 1
3	1, 2	lem3.1 443	1 (a v (a' ^ (a v b))) = (a v b)

Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  omln 446  oml5 449  oml2 451  ud1lem2 561  ud2lem2 564  ud3lem2 571  ud4lem2 582  ud5lem3 594  test 802  2oalem1 825  oas 925  oat 927  lem4.6.6i2j4 1094

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

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42

Copyright terms: Public domain