Theorem hlol 33666

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

Syntax hints:   → wi 4   ∈ wcel 1977  OLcol 33479  OMLcoml 33480  HLchlt 33655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-oml 33484  df-hlat 33656

This theorem is referenced by:  hlop  33667  cvrexch  33724  atle  33740  athgt  33760  2at0mat0  33829  dalem24  34001  pmapjat1  34157  atmod1i1m  34162  llnexchb2lem  34172  dalawlem2  34176  dalawlem6  34180  dalawlem7  34181  dalawlem11  34185  dalawlem12  34186  poldmj1N  34232  pmapj2N  34233  2polatN  34236  lhpmcvr3  34329  lhp2at0  34336  lhp2at0nle  34339  lhpelim  34341  lhpmod2i2  34342  lhpmod6i1  34343  lhprelat3N  34344  lhple  34346  4atex2-0aOLDN  34382  trljat1  34471  trljat2  34472  cdlemc1  34496  cdlemc6  34501  cdleme0cp  34519  cdleme0cq  34520  cdleme0e  34522  cdleme1  34532  cdleme2  34533  cdleme3c  34535  cdleme4  34543  cdleme5  34545  cdleme7c  34550  cdleme7e  34552  cdleme8  34555  cdleme9  34558  cdleme10  34559  cdleme15b  34580  cdlemednpq  34604  cdleme20yOLD  34608  cdleme20c  34617  cdleme20d  34618  cdleme20j  34624  cdleme22cN  34648  cdleme22d  34649  cdleme22e  34650  cdleme22eALTN  34651  cdleme23b  34656  cdleme30a  34684  cdlemefrs29pre00  34701  cdlemefrs29bpre0  34702  cdlemefrs29cpre1  34704  cdleme32fva  34743  cdleme35b  34756  cdleme35d  34758  cdleme35e  34759  cdleme42a  34777  cdleme42ke  34791  cdlemeg46frv  34831  cdlemg2fv2  34906  cdlemg2m  34910  cdlemg10bALTN  34942  cdlemg12e  34953  cdlemg31d  35006  trlcoabs2N  35028  trlcolem  35032  trljco  35046  cdlemh2  35122  cdlemh  35123  cdlemi1  35124  cdlemk4  35140  cdlemk9  35145  cdlemk9bN  35146  cdlemkid2  35230  dia2dimlem1  35371  dia2dimlem2  35372  dia2dimlem3  35373  doca2N  35433  djajN  35444  cdlemn10  35513  dihvalcqat  35546  dih1  35593  dihglbcpreN  35607  dihmeetbclemN  35611  dihmeetlem7N  35617  dihjatc1  35618  djhlj  35708  djh01  35719  dihjatc  35724