Axiom ax-a3 31

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:  anass 69  or12 73  or32 75  or4 77  omlem1 119  omlem2 120  letr 129  ler 141  wa3 185  ka4lemo 220  sklem 222  lei3 238  mccune2 239  i5con 264  wql2lem2 281  oaidlem1 286  nom20 305  i5lei1 339  i5lei3 341  wler 373  wletr 378  ska2 414  ska4 415  ka4ot 417  woml6 418  oml5 431  oml6 470  df2i3 480  dfi3b 481  oi3ai3 485  i3lem3 488  lem4 493  i3abs1 504  i3th1 525  i3con 533  i3orlem6 539  ud1lem3 544  ud3lem1c 550  ud3lem2 553  ud3lem3 558  ud4lem1c 561  ud4lem1 563  ud5lem1 571  ud5lem2 572  ud5lem3 576  u1lemoa 602  u2lemoa 603  u3lemoa 604  u4lemoa 605  u5lemoa 606  u2lemona 608  u4lemona 610  u5lemona 611  u5lemob 616  u3lemonb 619  u4lemonb 620  u5lemonb 621  u5lembi 707  u4lem2 729  u5lem4 742  u4lem5 746  u3lem6 749  u4lem6 750  u24lem 752  u2lem7 755  u1lem11 762  u3lem8 765  u3lem9 766  u3lem11 768  u3lemax4 778  u3lemax5 779  test 784  3vth5 790  3vth7 792  3vded11 796  3vded21 799  3vded3 801  2oalem1 807  sa5 818  orbi 824  negantlem10 843  elimcons2 851  mhlemlem1 856  mhlem 858  mh 861  oau 909  oaidlem2 911  oaidlem2g 912  oa23 916  oa4to6lem1 940  oa3-2lema 958  oa3-2lemb 959  oa3-6lem 960  oagen1 994  mloa 998  4oagen1 1021

metamath.org