Axiom ax-a1 30

Description: Axiom for ortholattices. (Contributed by NM, 9-Aug-1997.)

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  66  con2  67  con3  68  oran  87  anor1  88  anor2  89  oridm  110  anabs  121  conb  122  di  126  qlhoml1a  143  qlhoml1b  144  lecon1  155  lecon2  156  comcom2  183  wa1  191  wcon2  208  wcon3  209  wwfh1  216  wwfh2  217  wwfh4  219  ska9  237  i3n1  249  i1i2  266  i2i1  267  i1i2con1  268  i1i2con2  269  i3i4  270  i4i3  271  i5con  272  bina1  282  bina2  283  nomcon0  301  nomcon1  302  nomcon2  303  nom40  325  k1-7  354  k1-8a  355  k1-8b  356  k1-5  360  2vwomr2  362  wdf-c1  383  wcomcom2  415  wcomcom5  420  wfh2  424  omln  446  omlan  448  comcom5  458  fh2  470  dfi4b  500  i3n2  501  i3con1  531  ud3lem2  571  u1lemc6  706  u1lemn1b  730  u1lem7  772  u2lem7  773  u3lem7  774  u1lem8  776  u1lem11  780  u1lem12  781  u2lem8  782  u3lem8  783  u3lem11  786  u3lem13a  789  u3lem13b  790  u3lem14mp  794  3vth4  807  3vth5  808  sa5  836  sadm3  838  i1orni1  847  negantlem2  849  negantlem3  850  negantlem4  851  negantlem6  854  negant0  857  negant2  858  negantlem9  859  negantlem10  861  gomaex3h3  904  gomaex3h6  907  gomaex3h8  909  gomaex3h10  911  gomaex3lem4  917  gomaex3  924  oat  927  oatr  928  oa4lem1  937  oa4lem2  938  oa6todual  952  oa6fromdual  953  oa6fromdualn  954  oa8todual  971  oa4to4u  973  oa4uto4g  975  oa3-6lem  980  oa3-3lem  981  oa3-u1lem  985  oa3-u2lem  986  oa3-2to2s  990  oa3-1to5  993  d3oa  995  axoa4a  1037  lem4.6.2e1  1082  wdcom  1105