Axiom ax-a3 32

Description: Axiom for ortholattices.

Assertion

Ref	Expression
ax-a3	((a ∪ b) ∪ c) = (a ∪ (b ∪ c))

Detailed syntax breakdown of Axiom ax-a3

Step	Hyp	Ref	Expression
1		wva	. . . 4 term  a
2		wvb	. . . 4 term  b
3	1, 2	wo 6	. . 3 term  (a ∪ b)
4		wvc	. . 3 term  c
5	3, 4	wo 6	. 2 term  ((a ∪ b) ∪ c)
6	2, 4	wo 6	. . 3 term  (b ∪ c)
7	1, 6	wo 6	. 2 term  (a ∪ (b ∪ c))
8	5, 7	wb 1	1 wff  ((a ∪ b) ∪ c) = (a ∪ (b ∪ c))

This axiom is referenced by:  orass 75  anass 76  or12 80  or32 82  or4 84  omlem1 127  omlem2 128  letr 137  ler 149  wa3 193  ka4lemo 228  sklem 230  lei3 246  mccune2 247  i5con 272  wql2lem2 289  oaidlem1 294  nom20 313  i5lei1 347  i5lei3 349  wler 391  wletr 396  ska2 432  ska4 433  ka4ot 435  woml6 436  oml5 449  oml6 488  df2i3 498  dfi3b 499  oi3ai3 503  i3lem3 506  lem4 511  i3abs1 522  i3th1 543  i3con 551  i3orlem6 557  ud1lem3 562  ud3lem1c 568  ud3lem2 571  ud3lem3 576  ud4lem1c 579  ud4lem1 581  ud5lem1 589  ud5lem2 590  ud5lem3 594  u1lemoa 620  u2lemoa 621  u3lemoa 622  u4lemoa 623  u5lemoa 624  u2lemona 626  u4lemona 628  u5lemona 629  u5lemob 634  u3lemonb 637  u4lemonb 638  u5lemonb 639  u5lembi 725  u4lem2 747  u5lem4 760  u4lem5 764  u3lem6 767  u4lem6 768  u24lem 770  u2lem7 773  u1lem11 780  u3lem8 783  u3lem9 784  u3lem11 786  u3lemax4 796  u3lemax5 797  test 802  3vth5 808  3vth7 810  3vded11 814  3vded21 817  3vded3 819  2oalem1 825  sa5 836  orbi 842  negantlem10 861  elimcons2 869  mhlemlem1 874  mhlem 876  mh 879  e2ast2 894  e2astlem1 895  oau 929  oaidlem2 931  oaidlem2g 932  oa23 936  oa4to6lem1 960  oa3-2lema 978  oa3-2lemb 979  oa3-6lem 980  oagen1 1014  mloa 1018  4oagen1 1041  lem3.3.7i0e1 1056  lem3.3.7i1e1 1059  lem3.3.7i1e2 1060  lem3.3.7i2e1 1062  lem3.3.7i2e2 1063  lem3.3.7i3e2 1066  lem4.6.6i1j3 1091  lem4.6.6i2j4 1094  lem4.6.6i3j0 1095  lem4.6.6i3j1 1096  lem4.6.6i4j2 1098  lem4.6.7 1100

Copyright terms: Public domain