Axiom ax-a2 31

Description: Axiom for ortholattices.

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  4oath1 1040  lem3.3.3lem1 1048  lem3.3.3lem2 1049  lem3.3.4 1052  lem3.3.7i0e1 1056  lem3.3.7i1e2 1060  lem3.3.7i3e2 1066  lem4.6.2e1 1079  lem4.6.6i1j3 1091  lem4.6.6i2j4 1094  lem4.6.6i3j0 1095  lem4.6.6i3j1 1096  lem4.6.6i4j2 1098

Copyright terms: Public domain