Axiom ax-a3 32

Description: Axiom for ortholattices.

Assertion

Ref	Expression
ax-a3	((a v b) v c) = (a v (b v 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 v b)
4		wvc	. . 3 term c
5	3, 4	wo 6	. 2 term ((a v b) v c)
6	2, 4	wo 6	. . 3 term (b v c)
7	1, 6	wo 6	. 2 term (a v (b v c))
8	5, 7	wb 1	1 wff ((a v b) v c) = (a v (b v c))

This axiom is referenced by:  anass 70  or12 74  or32 76  or4 78  omlem1 121  omlem2 122  letr 131  ler 143  wa3 187  ka4lemo 222  sklem 224  lei3 240  mccune2 241  i5con 266  wql2lem2 283  oaidlem1 288  nom20 307  i5lei1 341  i5lei3 343  wler 377  wletr 382  ska2 418  ska4 419  ka4ot 421  woml6 422  oml5 435  oml6 474  df2i3 484  dfi3b 485  oi3ai3 489  i3lem3 492  lem4 497  i3abs1 508  i3th1 529  i3con 537  i3orlem6 543  ud1lem3 548  ud3lem1c 554  ud3lem2 557  ud3lem3 562  ud4lem1c 565  ud4lem1 567  ud5lem1 575  ud5lem2 576  ud5lem3 580  u1lemoa 606  u2lemoa 607  u3lemoa 608  u4lemoa 609  u5lemoa 610  u2lemona 612  u4lemona 614  u5lemona 615  u5lemob 620  u3lemonb 623  u4lemonb 624  u5lemonb 625  u5lembi 711  u4lem2 733  u5lem4 746  u4lem5 750  u3lem6 753  u4lem6 754  u24lem 756  u2lem7 759  u1lem11 766  u3lem8 769  u3lem9 770  u3lem11 772  u3lemax4 782  u3lemax5 783  test 788  3vth5 794  3vth7 796  3vded11 800  3vded21 803  3vded3 805  2oalem1 811  sa5 822  orbi 828  negantlem10 847  elimcons2 855  mhlemlem1 860  mhlem 862  mh 865  e2ast2 880  e2astlem1 881  oau 915  oaidlem2 917  oaidlem2g 918  oa23 922  oa4to6lem1 946  oa3-2lema 964  oa3-2lemb 965  oa3-6lem 966  oagen1 1000  mloa 1004  4oagen1 1027  lem3.3.7i0e1 1042  lem3.3.7i1e1 1045  lem3.3.7i1e2 1046  lem3.3.7i2e1 1048  lem3.3.7i2e2 1049  lem3.3.7i3e2 1052  lem4.6.6i1j3 1077  lem4.6.6i2j4 1080  lem4.6.6i3j0 1081  lem4.6.6i3j1 1082  lem4.6.6i4j2 1084  lem4.6.7 1086

Copyright terms: Public domain