Theorem wlan 370

Description: Weak orthomodular law.

Hypothesis

Ref	Expression
wlan.1	(a == b) = 1

Assertion

Ref	Expression
wlan	((c ^ a) == (c ^ b)) = 1

Proof of Theorem wlan

Step	Hyp	Ref	Expression
1		ancom 74	. . 3 (c ^ a) = (a ^ c)
2		ancom 74	. . 3 (c ^ b) = (b ^ c)
3	1, 2	2bi 99	. 2 ((c ^ a) == (c ^ b)) = ((a ^ c) == (b ^ c))
4		wlan.1	. . 3 (a == b) = 1
5	4	wran 369	. 2 ((a ^ c) == (b ^ c)) = 1
6	3, 5	ax-r2 36	1 ((c ^ a) == (c ^ b)) = 1

Syntax hints:   = wb 1   == tb 5   ^ wa 7  1wt 8

This theorem is referenced by:  w2an 373  wleoa 376  wom4 380  wcomlem 382  wletr 396  wlbtr 398  wcbtr 411  wcomcom2 415  wcom3ii 419  wfh1 423  wfh2 424  wlem14 430  wdid0id1 1109  wdid0id3 1111  wdid0id4 1112

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

Copyright terms: Public domain