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 66  con2 67  con3 68  oran 87  anor1 88  anor2 89  oridm 110  a5c 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 1036  lem4.6.2e1 1079  wdcom 1102

Copyright terms: Public domain