Axiom ax-a2 30

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 59  lor 66  ancom 68  or12 73  or32 75  or0 94  or0r 95  or1r 97  conb 114  leao 116  mi 117  omlem1 119  omlem2 120  lebi 137  le0 139  lerr 142  lecon 146  leor 151  lea 152  lelor 158  ledio 168  ledior 169  comm0 170  comcom2 175  wa2 184  wlem3.1 202  wwcomd 206  wwcom3ii 207  ska2a 218  ka4lemo 220  sklem 222  ska3 224  ska13 233  skr0 234  wlem1 235  ska15 236  lei3 238  mccune2 239  i3id 243  i3i4 262  i5con 264  0i1 265  1i1 266  i1id 267  bina4 277  wql2lem 280  wql2lem2 281  wql2lem4 283  wql1 285  womle2a 287  nomb41 291  nomb32 292  nomcon0 293  nomcon1 294  nomcon2 295  nom12 301  nom14 303  nom15 304  nom22 307  nom25 310  nom40 317  i5lei1 339  i5lei3 341  wlor 350  wcomlem 364  wdf-c1 365  wle0 372  wlecon 377  wlebi 384  wle2or 385  wledio 388  wcomcom2 397  wcom3ii 401  wcom3i 404  wnbdi 411  wlem14 412  ska2 414  ska4 415  woml6 418  woml7 419  lem3.1 425  oml5a 432  comcom 435  com3ii 439  comor2 444  com3i 449  fh3r 457  fh4r 458  fh2c 459  fh1rc 461  fh2rc 462  nbdi 468  oml6 470  gsth 471  gsth2 472  cmtr1com 475  i0cmtrcom 477  i3bi 478  df2i3 480  dfi3b 481  dfi4b 482  oi3ai3 485  i3lem1 486  i3lem3 488  i3abs3 506  i3orcom 507  i3th1 525  i3th5 529  i3con 533  i3orlem3 536  ud1lem1 542  ud1lem2 543  ud1lem3 544  ud2lem1 545  ud3lem1a 548  ud3lem1b 549  ud3lem1c 550  ud3lem1 552  ud3lem2 553  ud3lem3c 556  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1d 562  ud4lem1 563  ud4lem2 564  ud4lem3b 566  ud4lem3 567  ud5lem1a 568  ud5lem1b 569  ud5lem1c 570  ud5lem2 572  ud5lem3a 573  ud5lem3 576  u1lemaa 582  u2lemaa 583  u3lemaa 584  u5lemaa 586  u2lemana 588  u4lemana 590  u5lemana 591  u1lemab 592  u3lemab 594  u1lemanb 597  u2lemanb 598  u3lemanb 599  u4lemanb 600  u5lemanb 601  u1lemoa 602  u2lemoa 603  u3lemoa 604  u4lemoa 605  u5lemoa 606  u2lemona 608  u5lemona 611  u1lemob 612  u2lemob 613  u3lemob 614  u2lemonb 618  u3lemonb 619  u3lemnana 629  u5lemnana 631  u4lemnab 635  u5lemnab 636  u2lemnoa 643  u3lemnoa 644  u4lemnoa 645  u5lemnoa 646  u1lemnonb 657  u3lemnonb 659  u4lemnonb 660  u5lemnonb 661  u1lemc4 683  u2lemc4 684  u3lemc4 685  u4lemc4 686  u5lemc4 687  comi1 691  u1lemle2 697  u2lemle2 698  u1lembi 702  u5lembi 707  u21lembi 709  u1lem3var1 713  oi3oa3 715  u2lem1 717  u1lem2 726  u3lem2 728  u4lem2 729  u5lem2 730  u3lem3 733  u4lem3 734  u5lem3 735  u3lem3n 736  u4lem3n 737  u5lem3n 738  u1lem4 739  u3lem4 740  u3lem5 745  u4lem5 746  u4lem6 750  u2lem7 755  u3lem7 756  u2lem7n 757  u1lem8 758  u1lem11 762  u3lem8 765  u3lem11 768  u3lem13a 771  u3lem13b 772  u3lem14a 773  bi1o1a 780  i2i1i1 782  test 784  test2 785  3vth2 787  3vth3 788  3vth6 791  3vth9 794  3vded21 799  1oa 802  1oaiii 805  2oalem1 807  oale 811  sa5 818  salem1 819  orbi 824  negantlem10 843  neg3antlem2 847  elimconslem 849  elimcons2 851  mhlemlem2 857  mhlem 858  mhlem1 859  mhlem2 860  mh 861  mlaconjolem 867  distid 869  mhcor1 870  govar 876  gomaex4 880  gomaex3lem2 895  gomaex3lem3 896  gomaex3lem7 900  gomaex3 904  oau 909  oaidlem2 911  oaidlem2g 912  oa4v3v 914  oa23 916  oa4lem1 917  oa4lem2 918  oa3to4lem1 925  oa3to4lem2 926  oa3to4lem5 929  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oa4to4u 953  oa4uto4 957  oa3-2lema 958  oa3-1lem 962  oa3-4lem 963  oa3-u1lem 965  oa3-u2lem 966  oa3-6to3 967  oa3-2to4 968  oa3-u1 971  oa3-1to5 973  d3oa 975  d4oa 976  oaliii 981  oath1 984  oalem2 986  oadist2a 987  oadistc0 1001  3oa2 1004  4oath1 1020

metamath.org