Theorem hlol 39734

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

Syntax hints:   → wi 4   ∈ wcel 2114  OLcol 39547  OMLcoml 39548  HLchlt 39723

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-oml 39552  df-hlat 39724

This theorem is referenced by:  hlop  39735  cvrexch  39793  atle  39809  athgt  39829  2at0mat0  39898  dalem24  40070  pmapjat1  40226  atmod1i1m  40231  llnexchb2lem  40241  dalawlem2  40245  dalawlem6  40249  dalawlem7  40250  dalawlem11  40254  dalawlem12  40255  poldmj1N  40301  pmapj2N  40302  2polatN  40305  lhpmcvr3  40398  lhp2at0  40405  lhp2at0nle  40408  lhpelim  40410  lhpmod2i2  40411  lhpmod6i1  40412  lhprelat3N  40413  lhple  40415  4atex2-0aOLDN  40451  trljat1  40539  trljat2  40540  cdlemc1  40564  cdlemc6  40569  cdleme0cp  40587  cdleme0cq  40588  cdleme0e  40590  cdleme1  40600  cdleme2  40601  cdleme3c  40603  cdleme4  40611  cdleme5  40613  cdleme7c  40618  cdleme7e  40620  cdleme8  40623  cdleme9  40626  cdleme10  40627  cdleme15b  40648  cdlemednpq  40672  cdleme20c  40684  cdleme20d  40685  cdleme20j  40691  cdleme22cN  40715  cdleme22d  40716  cdleme22e  40717  cdleme22eALTN  40718  cdleme23b  40723  cdleme30a  40751  cdlemefrs29pre00  40768  cdlemefrs29bpre0  40769  cdlemefrs29cpre1  40771  cdleme32fva  40810  cdleme35b  40823  cdleme35d  40825  cdleme35e  40826  cdleme42a  40844  cdleme42ke  40858  cdlemeg46frv  40898  cdlemg2fv2  40973  cdlemg2m  40977  cdlemg10bALTN  41009  cdlemg12e  41020  cdlemg31d  41073  trlcoabs2N  41095  trlcolem  41099  trljco  41113  cdlemh2  41189  cdlemh  41190  cdlemi1  41191  cdlemk4  41207  cdlemk9  41212  cdlemk9bN  41213  cdlemkid2  41297  dia2dimlem1  41437  dia2dimlem2  41438  dia2dimlem3  41439  doca2N  41499  djajN  41510  cdlemn10  41579  dihvalcqat  41612  dih1  41659  dihglbcpreN  41673  dihmeetbclemN  41677  dihmeetlem7N  41683  dihjatc1  41684  djhlj  41774  djh01  41785  dihjatc  41790