Theorem hlol 38219

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 38215	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OML)
2		omlol 38098	. 2 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)

Syntax hints:   → wi 4   ∈ wcel 2106  OLcol 38032  OMLcoml 38033  HLchlt 38208

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-oml 38037  df-hlat 38209

This theorem is referenced by:  hlop  38220  cvrexch  38279  atle  38295  athgt  38315  2at0mat0  38384  dalem24  38556  pmapjat1  38712  atmod1i1m  38717  llnexchb2lem  38727  dalawlem2  38731  dalawlem6  38735  dalawlem7  38736  dalawlem11  38740  dalawlem12  38741  poldmj1N  38787  pmapj2N  38788  2polatN  38791  lhpmcvr3  38884  lhp2at0  38891  lhp2at0nle  38894  lhpelim  38896  lhpmod2i2  38897  lhpmod6i1  38898  lhprelat3N  38899  lhple  38901  4atex2-0aOLDN  38937  trljat1  39025  trljat2  39026  cdlemc1  39050  cdlemc6  39055  cdleme0cp  39073  cdleme0cq  39074  cdleme0e  39076  cdleme1  39086  cdleme2  39087  cdleme3c  39089  cdleme4  39097  cdleme5  39099  cdleme7c  39104  cdleme7e  39106  cdleme8  39109  cdleme9  39112  cdleme10  39113  cdleme15b  39134  cdlemednpq  39158  cdleme20c  39170  cdleme20d  39171  cdleme20j  39177  cdleme22cN  39201  cdleme22d  39202  cdleme22e  39203  cdleme22eALTN  39204  cdleme23b  39209  cdleme30a  39237  cdlemefrs29pre00  39254  cdlemefrs29bpre0  39255  cdlemefrs29cpre1  39257  cdleme32fva  39296  cdleme35b  39309  cdleme35d  39311  cdleme35e  39312  cdleme42a  39330  cdleme42ke  39344  cdlemeg46frv  39384  cdlemg2fv2  39459  cdlemg2m  39463  cdlemg10bALTN  39495  cdlemg12e  39506  cdlemg31d  39559  trlcoabs2N  39581  trlcolem  39585  trljco  39599  cdlemh2  39675  cdlemh  39676  cdlemi1  39677  cdlemk4  39693  cdlemk9  39698  cdlemk9bN  39699  cdlemkid2  39783  dia2dimlem1  39923  dia2dimlem2  39924  dia2dimlem3  39925  doca2N  39985  djajN  39996  cdlemn10  40065  dihvalcqat  40098  dih1  40145  dihglbcpreN  40159  dihmeetbclemN  40163  dihmeetlem7N  40169  dihjatc1  40170  djhlj  40260  djh01  40271  dihjatc  40276