Theorem hlol 38963

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

Syntax hints:   → wi 4   ∈ wcel 2098  OLcol 38776  OMLcoml 38777  HLchlt 38952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-ov 7422  df-oml 38781  df-hlat 38953

This theorem is referenced by:  hlop  38964  cvrexch  39023  atle  39039  athgt  39059  2at0mat0  39128  dalem24  39300  pmapjat1  39456  atmod1i1m  39461  llnexchb2lem  39471  dalawlem2  39475  dalawlem6  39479  dalawlem7  39480  dalawlem11  39484  dalawlem12  39485  poldmj1N  39531  pmapj2N  39532  2polatN  39535  lhpmcvr3  39628  lhp2at0  39635  lhp2at0nle  39638  lhpelim  39640  lhpmod2i2  39641  lhpmod6i1  39642  lhprelat3N  39643  lhple  39645  4atex2-0aOLDN  39681  trljat1  39769  trljat2  39770  cdlemc1  39794  cdlemc6  39799  cdleme0cp  39817  cdleme0cq  39818  cdleme0e  39820  cdleme1  39830  cdleme2  39831  cdleme3c  39833  cdleme4  39841  cdleme5  39843  cdleme7c  39848  cdleme7e  39850  cdleme8  39853  cdleme9  39856  cdleme10  39857  cdleme15b  39878  cdlemednpq  39902  cdleme20c  39914  cdleme20d  39915  cdleme20j  39921  cdleme22cN  39945  cdleme22d  39946  cdleme22e  39947  cdleme22eALTN  39948  cdleme23b  39953  cdleme30a  39981  cdlemefrs29pre00  39998  cdlemefrs29bpre0  39999  cdlemefrs29cpre1  40001  cdleme32fva  40040  cdleme35b  40053  cdleme35d  40055  cdleme35e  40056  cdleme42a  40074  cdleme42ke  40088  cdlemeg46frv  40128  cdlemg2fv2  40203  cdlemg2m  40207  cdlemg10bALTN  40239  cdlemg12e  40250  cdlemg31d  40303  trlcoabs2N  40325  trlcolem  40329  trljco  40343  cdlemh2  40419  cdlemh  40420  cdlemi1  40421  cdlemk4  40437  cdlemk9  40442  cdlemk9bN  40443  cdlemkid2  40527  dia2dimlem1  40667  dia2dimlem2  40668  dia2dimlem3  40669  doca2N  40729  djajN  40740  cdlemn10  40809  dihvalcqat  40842  dih1  40889  dihglbcpreN  40903  dihmeetbclemN  40907  dihmeetlem7N  40913  dihjatc1  40914  djhlj  41004  djh01  41015  dihjatc  41020