Theorem oml 431

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 121	. 2 ((a v (a' ^ (a v b))) v (a v b)) = (a v b)
2		omlem2 122	. 2 ((a v b)' v (a v (a' ^ (a v b)))) = 1
3	1, 2	lem3.1 429	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 432  oml5 435  oml2 437  ud1lem2 547  ud2lem2 550  ud3lem2 557  ud4lem2 568  ud5lem3 580  test 788  2oalem1 811  oas 911  oat 913  lem4.6.6i2j4 1080

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 425

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

Copyright terms: Public domain