Theorem hlol 39821

Description: A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.)

Assertion

Ref	Expression
hlol	⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)

Proof of Theorem hlol

Step	Hyp	Ref	Expression
1		hloml 39817	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OML)
2		omlol 39700	. 2 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)

Syntax hints:   → wi 4   ∈ wcel 2114  OLcol 39634  OMLcoml 39635  HLchlt 39810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-oml 39639  df-hlat 39811

This theorem is referenced by:  hlop  39822  cvrexch  39880  atle  39896  athgt  39916  2at0mat0  39985  dalem24  40157  pmapjat1  40313  atmod1i1m  40318  llnexchb2lem  40328  dalawlem2  40332  dalawlem6  40336  dalawlem7  40337  dalawlem11  40341  dalawlem12  40342  poldmj1N  40388  pmapj2N  40389  2polatN  40392  lhpmcvr3  40485  lhp2at0  40492  lhp2at0nle  40495  lhpelim  40497  lhpmod2i2  40498  lhpmod6i1  40499  lhprelat3N  40500  lhple  40502  4atex2-0aOLDN  40538  trljat1  40626  trljat2  40627  cdlemc1  40651  cdlemc6  40656  cdleme0cp  40674  cdleme0cq  40675  cdleme0e  40677  cdleme1  40687  cdleme2  40688  cdleme3c  40690  cdleme4  40698  cdleme5  40700  cdleme7c  40705  cdleme7e  40707  cdleme8  40710  cdleme9  40713  cdleme10  40714  cdleme15b  40735  cdlemednpq  40759  cdleme20c  40771  cdleme20d  40772  cdleme20j  40778  cdleme22cN  40802  cdleme22d  40803  cdleme22e  40804  cdleme22eALTN  40805  cdleme23b  40810  cdleme30a  40838  cdlemefrs29pre00  40855  cdlemefrs29bpre0  40856  cdlemefrs29cpre1  40858  cdleme32fva  40897  cdleme35b  40910  cdleme35d  40912  cdleme35e  40913  cdleme42a  40931  cdleme42ke  40945  cdlemeg46frv  40985  cdlemg2fv2  41060  cdlemg2m  41064  cdlemg10bALTN  41096  cdlemg12e  41107  cdlemg31d  41160  trlcoabs2N  41182  trlcolem  41186  trljco  41200  cdlemh2  41276  cdlemh  41277  cdlemi1  41278  cdlemk4  41294  cdlemk9  41299  cdlemk9bN  41300  cdlemkid2  41384  dia2dimlem1  41524  dia2dimlem2  41525  dia2dimlem3  41526  doca2N  41586  djajN  41597  cdlemn10  41666  dihvalcqat  41699  dih1  41746  dihglbcpreN  41760  dihmeetbclemN  41764  dihmeetlem7N  41770  dihjatc1  41771  djhlj  41861  djh01  41872  dihjatc  41877