Theorem hlol 39362

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

Syntax hints:   → wi 4   ∈ wcel 2108  OLcol 39175  OMLcoml 39176  HLchlt 39351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-oml 39180  df-hlat 39352

This theorem is referenced by:  hlop  39363  cvrexch  39422  atle  39438  athgt  39458  2at0mat0  39527  dalem24  39699  pmapjat1  39855  atmod1i1m  39860  llnexchb2lem  39870  dalawlem2  39874  dalawlem6  39878  dalawlem7  39879  dalawlem11  39883  dalawlem12  39884  poldmj1N  39930  pmapj2N  39931  2polatN  39934  lhpmcvr3  40027  lhp2at0  40034  lhp2at0nle  40037  lhpelim  40039  lhpmod2i2  40040  lhpmod6i1  40041  lhprelat3N  40042  lhple  40044  4atex2-0aOLDN  40080  trljat1  40168  trljat2  40169  cdlemc1  40193  cdlemc6  40198  cdleme0cp  40216  cdleme0cq  40217  cdleme0e  40219  cdleme1  40229  cdleme2  40230  cdleme3c  40232  cdleme4  40240  cdleme5  40242  cdleme7c  40247  cdleme7e  40249  cdleme8  40252  cdleme9  40255  cdleme10  40256  cdleme15b  40277  cdlemednpq  40301  cdleme20c  40313  cdleme20d  40314  cdleme20j  40320  cdleme22cN  40344  cdleme22d  40345  cdleme22e  40346  cdleme22eALTN  40347  cdleme23b  40352  cdleme30a  40380  cdlemefrs29pre00  40397  cdlemefrs29bpre0  40398  cdlemefrs29cpre1  40400  cdleme32fva  40439  cdleme35b  40452  cdleme35d  40454  cdleme35e  40455  cdleme42a  40473  cdleme42ke  40487  cdlemeg46frv  40527  cdlemg2fv2  40602  cdlemg2m  40606  cdlemg10bALTN  40638  cdlemg12e  40649  cdlemg31d  40702  trlcoabs2N  40724  trlcolem  40728  trljco  40742  cdlemh2  40818  cdlemh  40819  cdlemi1  40820  cdlemk4  40836  cdlemk9  40841  cdlemk9bN  40842  cdlemkid2  40926  dia2dimlem1  41066  dia2dimlem2  41067  dia2dimlem3  41068  doca2N  41128  djajN  41139  cdlemn10  41208  dihvalcqat  41241  dih1  41288  dihglbcpreN  41302  dihmeetbclemN  41306  dihmeetlem7N  41312  dihjatc1  41313  djhlj  41403  djh01  41414  dihjatc  41419