Axiom ax-a1 29

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 58  con1 63  con2 64  con3 65  oran 79  anor1 80  anor2 81  oridm 102  a5c 113  conb 114  di 118  qlhoml1a 135  qlhoml1b 136  lecon1 147  lecon2 148  comcom2 175  wa1 183  wcon2 200  wcon3 201  wwfh1 208  wwfh2 209  wwfh4 211  ska9 229  i3n1 241  i1i2 258  i2i1 259  i1i2con1 260  i1i2con2 261  i3i4 262  i4i3 263  i5con 264  bina1 274  bina2 275  nomcon0 293  nomcon1 294  nomcon2 295  nom40 317  2vwomr2 344  wdf-c1 365  wcomcom2 397  wcomcom5 402  wfh2 406  omln 428  omlan 430  comcom5 440  fh2 452  dfi4b 482  i3n2 483  i3con1 513  ud3lem2 553  u1lemc6 688  u1lemn1b 712  u1lem7 754  u2lem7 755  u3lem7 756  u1lem8 758  u1lem11 762  u1lem12 763  u2lem8 764  u3lem8 765  u3lem11 768  u3lem13a 771  u3lem13b 772  u3lem14mp 776  3vth4 789  3vth5 790  sa5 818  sadm3 820  i1orni1 829  negantlem2 831  negantlem3 832  negantlem4 833  negantlem6 836  negant0 839  negant2 840  negantlem9 841  negantlem10 843  gomaex3h3 884  gomaex3h6 887  gomaex3h8 889  gomaex3h10 891  gomaex3lem4 897  gomaex3 904  oat 907  oatr 908  oa4lem1 917  oa4lem2 918  oa6todual 932  oa6fromdual 933  oa6fromdualn 934  oa8todual 951  oa4to4u 953  oa4uto4g 955  oa3-6lem 960  oa3-3lem 961  oa3-u1lem 965  oa3-u2lem 966  oa3-2to2s 970  oa3-1to5 973  d3oa 975  axoa4a 1016

metamath.org