Axiom ax-a1 30

Description: Axiom for ortholattices.

Assertion

Ref	Expression
ax-a1	a = a''

Detailed syntax breakdown of Axiom ax-a1

Step	Hyp	Ref	Expression
1		wva	. 2 term a
2	1	wn 4	. . 3 term a'
3	2	wn 4	. 2 term a''
4	1, 3	wb 1	1 wff a = a''

This axiom is referenced by:  id 59  con1 64  con2 65  con3 66  oran 81  anor1 82  anor2 83  oridm 104  a5c 115  conb 116  di 120  qlhoml1a 137  qlhoml1b 138  lecon1 149  lecon2 150  comcom2 177  wa1 185  wcon2 202  wcon3 203  wwfh1 210  wwfh2 211  wwfh4 213  ska9 231  i3n1 243  i1i2 260  i2i1 261  i1i2con1 262  i1i2con2 263  i3i4 264  i4i3 265  i5con 266  bina1 276  bina2 277  nomcon0 295  nomcon1 296  nomcon2 297  nom40 319  2vwomr2 348  wdf-c1 369  wcomcom2 401  wcomcom5 406  wfh2 410  omln 432  omlan 434  comcom5 444  fh2 456  dfi4b 486  i3n2 487  i3con1 517  ud3lem2 557  u1lemc6 692  u1lemn1b 716  u1lem7 758  u2lem7 759  u3lem7 760  u1lem8 762  u1lem11 766  u1lem12 767  u2lem8 768  u3lem8 769  u3lem11 772  u3lem13a 775  u3lem13b 776  u3lem14mp 780  3vth4 793  3vth5 794  sa5 822  sadm3 824  i1orni1 833  negantlem2 835  negantlem3 836  negantlem4 837  negantlem6 840  negant0 843  negant2 844  negantlem9 845  negantlem10 847  gomaex3h3 890  gomaex3h6 893  gomaex3h8 895  gomaex3h10 897  gomaex3lem4 903  gomaex3 910  oat 913  oatr 914  oa4lem1 923  oa4lem2 924  oa6todual 938  oa6fromdual 939  oa6fromdualn 940  oa8todual 957  oa4to4u 959  oa4uto4g 961  oa3-6lem 966  oa3-3lem 967  oa3-u1lem 971  oa3-u2lem 972  oa3-2to2s 976  oa3-1to5 979  d3oa 981  axoa4a 1022  lem4.6.2e1 1065  wdcom 1088

Copyright terms: Public domain