Axiom ax-a2 31

Description: Axiom for ortholattices.

Assertion

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

This axiom is referenced by:  tt 60  lor 67  ancom 69  or12 74  or32 76  or42 79  or0 96  or0r 97  or1r 99  conb 116  leao 118  mi 119  omlem1 121  omlem2 122  lebi 139  le0 141  lerr 144  lecon 148  leor 153  lea 154  lelor 160  ledio 170  ledior 171  comm0 172  comcom2 177  wa2 186  wlem3.1 204  wwcomd 208  wwcom3ii 209  anorabs 219  ska2a 220  ka4lemo 222  sklem 224  ska3 226  ska13 235  skr0 236  wlem1 237  ska15 238  lei3 240  mccune2 241  i3id 245  i3i4 264  i5con 266  0i1 267  1i1 268  i1id 269  bina4 279  wql2lem 282  wql2lem2 283  wql2lem4 285  wql1 287  womle2a 289  nomb41 293  nomb32 294  nomcon0 295  nomcon1 296  nomcon2 297  nom12 303  nom14 305  nom15 306  nom22 309  nom25 312  nom40 319  i5lei1 341  i5lei3 343  id5leid0 345  wlor 354  wcomlem 368  wdf-c1 369  wle0 376  wlecon 381  wlebi 388  wle2or 389  wledio 392  wcomcom2 401  wcom3ii 405  wcom3i 408  wnbdi 415  wlem14 416  ska2 418  ska4 419  woml6 422  woml7 423  oml5a 436  comcom 439  com3ii 443  comor2 448  com3i 453  fh3r 461  fh4r 462  fh2c 463  fh1rc 465  fh2rc 466  nbdi 472  oml6 474  gsth 475  gsth2 476  cmtr1com 479  i0cmtrcom 481  i3bi 482  df2i3 484  dfi3b 485  dfi4b 486  oi3ai3 489  i3lem1 490  i3lem3 492  i3abs3 510  i3orcom 511  i3th1 529  i3th5 533  i3con 537  i3orlem3 540  ud1lem1 546  ud1lem2 547  ud1lem3 548  ud2lem1 549  ud3lem1a 552  ud3lem1b 553  ud3lem1c 554  ud3lem1 556  ud3lem2 557  ud3lem3c 560  ud3lem3 562  ud4lem1a 563  ud4lem1b 564  ud4lem1c 565  ud4lem1d 566  ud4lem1 567  ud4lem2 568  ud4lem3b 570  ud4lem3 571  ud5lem1a 572  ud5lem1b 573  ud5lem1c 574  ud5lem2 576  ud5lem3a 577  ud5lem3 580  u1lemaa 586  u2lemaa 587  u3lemaa 588  u5lemaa 590  u2lemana 592  u4lemana 594  u5lemana 595  u1lemab 596  u3lemab 598  u1lemanb 601  u2lemanb 602  u3lemanb 603  u4lemanb 604  u5lemanb 605  u1lemoa 606  u2lemoa 607  u3lemoa 608  u4lemoa 609  u5lemoa 610  u2lemona 612  u5lemona 615  u1lemob 616  u2lemob 617  u3lemob 618  u2lemonb 622  u3lemonb 623  u3lemnana 633  u5lemnana 635  u4lemnab 639  u5lemnab 640  u2lemnoa 647  u3lemnoa 648  u4lemnoa 649  u5lemnoa 650  u1lemnonb 661  u3lemnonb 663  u4lemnonb 664  u5lemnonb 665  u1lemc4 687  u2lemc4 688  u3lemc4 689  u4lemc4 690  u5lemc4 691  comi1 695  u1lemle2 701  u2lemle2 702  u1lembi 706  u5lembi 711  u21lembi 713  u1lem3var1 717  oi3oa3 719  u2lem1 721  u1lem2 730  u3lem2 732  u4lem2 733  u5lem2 734  u3lem3 737  u4lem3 738  u5lem3 739  u3lem3n 740  u4lem3n 741  u5lem3n 742  u1lem4 743  u3lem4 744  u3lem5 749  u4lem5 750  u4lem6 754  u2lem7 759  u3lem7 760  u2lem7n 761  u1lem8 762  u1lem11 766  u3lem8 769  u3lem11 772  u3lem13a 775  u3lem13b 776  u3lem14a 777  bi1o1a 784  i2i1i1 786  test 788  test2 789  3vth2 791  3vth3 792  3vth6 795  3vth9 798  3vded21 803  1oa 806  1oaiii 809  2oalem1 811  oale 815  sa5 822  salem1 823  orbi 828  negantlem10 847  neg3antlem2 851  elimconslem 853  elimcons2 855  mhlemlem2 861  mhlem 862  mhlem1 863  mhlem2 864  mh 865  mlaconjolem 871  distid 873  mhcor1 874  e2ast2 880  govar 882  gomaex4 886  gomaex3lem2 901  gomaex3lem3 902  gomaex3lem7 906  gomaex3 910  oau 915  oaidlem2 917  oaidlem2g 918  oa4v3v 920  oa23 922  oa4lem1 923  oa4lem2 924  oa3to4lem1 931  oa3to4lem2 932  oa3to4lem5 935  oa4to6lem1 946  oa4to6lem2 947  oa4to6lem3 948  oa4to4u 959  oa4uto4 963  oa3-2lema 964  oa3-1lem 968  oa3-4lem 969  oa3-u1lem 971  oa3-u2lem 972  oa3-6to3 973  oa3-2to4 974  oa3-u1 977  oa3-1to5 979  d3oa 981  d4oa 982  oaliii 987  oath1 990  oalem2 992  oadist2a 993  oadistc0 1007  3oa2 1010  4oath1 1026  lem3.3.3lem1 1034  lem3.3.3lem2 1035  lem3.3.4 1038  lem3.3.7i0e1 1042  lem3.3.7i1e2 1046  lem3.3.7i3e2 1052  lem4.6.2e1 1065  lem4.6.6i1j3 1077  lem4.6.6i2j4 1080  lem4.6.6i3j0 1081  lem4.6.6i3j1 1082  lem4.6.6i4j2 1084

Copyright terms: Public domain