Axiom ax-a2 31

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

Assertion

Ref	Expression
ax-a2	(a ∪ b) = (b ∪ a)

Detailed syntax breakdown of Axiom ax-a2

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

This axiom is referenced by:  tt  60  lor  70  orcom  73  ancom  74  or12  80  or32  82  or42  85  or0  102  or0r  103  or1r  105  conb  122  leao  124  mi  125  omlem1  127  omlem2  128  lebi  145  le0  147  lerr  150  lecon  154  leor  159  lea  160  lelor  166  ledio  176  ledior  177  comm0  178  comcom2  183  wa2  192  wlem3.1  210  wwcomd  214  wwcom3ii  215  anorabs  225  ska2a  226  ka4lemo  228  sklem  230  ska3  232  ska13  241  skr0  242  wlem1  243  ska15  244  lei3  246  mccune2  247  i3id  251  i3i4  270  i5con  272  0i1  273  1i1  274  i1id  275  bina4  285  wql2lem  288  wql2lem2  289  wql2lem4  291  wql1  293  womle2a  295  nomb41  299  nomb32  300  nomcon0  301  nomcon1  302  nomcon2  303  nom12  309  nom14  311  nom15  312  nom22  315  nom25  318  nom40  325  i5lei1  347  i5lei3  349  id5leid0  351  k1-6  353  k1-7  354  wlor  368  wcomlem  382  wdf-c1  383  wle0  390  wlecon  395  wlebi  402  wle2or  403  wledio  406  wcomcom2  415  wcom3ii  419  wcom3i  422  wnbdi  429  wlem14  430  ska2  432  ska4  433  woml6  436  woml7  437  oml5a  450  comcom  453  com3ii  457  comor2  462  com3i  467  fh3r  475  fh4r  476  fh2c  477  fh1rc  479  fh2rc  480  nbdi  486  oml6  488  gsth  489  gsth2  490  cmtr1com  493  i0cmtrcom  495  i3bi  496  df2i3  498  dfi3b  499  dfi4b  500  oi3ai3  503  i3lem1  504  i3lem3  506  i3abs3  524  i3orcom  525  i3th1  543  i3th5  547  i3con  551  i3orlem3  554  ud1lem1  560  ud1lem2  561  ud1lem3  562  ud2lem1  563  ud3lem1a  566  ud3lem1b  567  ud3lem1c  568  ud3lem1  570  ud3lem2  571  ud3lem3c  574  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud4lem1d  580  ud4lem1  581  ud4lem2  582  ud4lem3b  584  ud4lem3  585  ud5lem1a  586  ud5lem1b  587  ud5lem1c  588  ud5lem2  590  ud5lem3a  591  ud5lem3  594  u1lemaa  600  u2lemaa  601  u3lemaa  602  u5lemaa  604  u2lemana  606  u4lemana  608  u5lemana  609  u1lemab  610  u3lemab  612  u1lemanb  615  u2lemanb  616  u3lemanb  617  u4lemanb  618  u5lemanb  619  u1lemoa  620  u2lemoa  621  u3lemoa  622  u4lemoa  623  u5lemoa  624  u2lemona  626  u5lemona  629  u1lemob  630  u2lemob  631  u3lemob  632  u2lemonb  636  u3lemonb  637  u3lemnana  647  u5lemnana  649  u4lemnab  653  u5lemnab  654  u2lemnoa  661  u3lemnoa  662  u4lemnoa  663  u5lemnoa  664  u1lemnonb  675  u3lemnonb  677  u4lemnonb  678  u5lemnonb  679  u1lemc4  701  u2lemc4  702  u3lemc4  703  u4lemc4  704  u5lemc4  705  comi1  709  u1lemle2  715  u2lemle2  716  u1lembi  720  u5lembi  725  u21lembi  727  u1lem3var1  731  oi3oa3  733  u2lem1  735  u1lem2  744  u3lem2  746  u4lem2  747  u5lem2  748  u3lem3  751  u4lem3  752  u5lem3  753  u3lem3n  754  u4lem3n  755  u5lem3n  756  u1lem4  757  u3lem4  758  u3lem5  763  u4lem5  764  u4lem6  768  u2lem7  773  u3lem7  774  u2lem7n  775  u1lem8  776  u1lem11  780  u3lem8  783  u3lem11  786  u3lem13a  789  u3lem13b  790  u3lem14a  791  bi1o1a  798  i2i1i1  800  test  802  test2  803  3vth2  805  3vth3  806  3vth6  809  3vth9  812  3vded21  817  1oa  820  1oaiii  823  2oalem1  825  oale  829  sa5  836  salem1  837  orbi  842  negantlem10  861  neg3antlem2  865  elimconslem  867  elimcons2  869  mhlemlem2  875  mhlem  876  mhlem1  877  mhlem2  878  mh  879  mlaconjolem  885  distid  887  mhcor1  888  e2ast2  894  govar  896  gomaex4  900  gomaex3lem2  915  gomaex3lem3  916  gomaex3lem7  920  gomaex3  924  oau  929  oaidlem2  931  oaidlem2g  932  oa4v3v  934  oa23  936  oa4lem1  937  oa4lem2  938  oa3to4lem1  945  oa3to4lem2  946  oa3to4lem5  949  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa4to4u  973  oa4uto4  977  oa3-2lema  978  oa3-1lem  982  oa3-4lem  983  oa3-u1lem  985  oa3-u2lem  986  oa3-6to3  987  oa3-2to4  988  oa3-u1  991  oa3-1to5  993  d3oa  995  d4oa  996  oaliii  1001  oath1  1004  oalem2  1006  oadist2a  1007  oadistc0  1021  3oa2  1024  oa3moa3  1029  4oath1  1041  lem3.3.3lem1  1049  lem3.3.3lem2  1050  lem3.3.4  1053  lem3.3.7i0e1  1057  lem3.3.7i1e2  1061  lem3.3.7i3e2  1067  thm3.8i1lem  1080  lem4.6.2e1  1082  lem4.6.6i1j3  1094  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j2  1101  mlduali  1128  vneulem2  1132  vneulem6  1136  vneulem10  1140  vneulem11  1141  vneulemexp  1148  dp15leme  1158  dp41lemc0  1184  dp41lemd  1186  dp41lemj  1191  xdp41  1198  xdp15  1199  xxdp41  1201  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208