Axiom ax-a3 32

Description: Axiom for ortholattices. (Contributed by NM, 9-Aug-1997.)

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  oa3moa3  1029  4oagen1  1042  lem3.3.7i0e1  1057  lem3.3.7i1e1  1060  lem3.3.7i1e2  1061  lem3.3.7i2e1  1063  lem3.3.7i2e2  1064  lem3.3.7i3e2  1067  lem4.6.6i1j3  1094  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j2  1101  lem4.6.7  1103  vneulem11  1141  vneulemexp  1148  dp53lema  1163  xdp53  1200  xxdp53  1203  xdp43lem  1205  xdp43  1207  3dp43  1208