Theorem hlol 39379

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

Syntax hints:   → wi 4   ∈ wcel 2108  OLcol 39192  OMLcoml 39193  HLchlt 39368

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-oml 39197  df-hlat 39369

This theorem is referenced by:  hlop  39380  cvrexch  39439  atle  39455  athgt  39475  2at0mat0  39544  dalem24  39716  pmapjat1  39872  atmod1i1m  39877  llnexchb2lem  39887  dalawlem2  39891  dalawlem6  39895  dalawlem7  39896  dalawlem11  39900  dalawlem12  39901  poldmj1N  39947  pmapj2N  39948  2polatN  39951  lhpmcvr3  40044  lhp2at0  40051  lhp2at0nle  40054  lhpelim  40056  lhpmod2i2  40057  lhpmod6i1  40058  lhprelat3N  40059  lhple  40061  4atex2-0aOLDN  40097  trljat1  40185  trljat2  40186  cdlemc1  40210  cdlemc6  40215  cdleme0cp  40233  cdleme0cq  40234  cdleme0e  40236  cdleme1  40246  cdleme2  40247  cdleme3c  40249  cdleme4  40257  cdleme5  40259  cdleme7c  40264  cdleme7e  40266  cdleme8  40269  cdleme9  40272  cdleme10  40273  cdleme15b  40294  cdlemednpq  40318  cdleme20c  40330  cdleme20d  40331  cdleme20j  40337  cdleme22cN  40361  cdleme22d  40362  cdleme22e  40363  cdleme22eALTN  40364  cdleme23b  40369  cdleme30a  40397  cdlemefrs29pre00  40414  cdlemefrs29bpre0  40415  cdlemefrs29cpre1  40417  cdleme32fva  40456  cdleme35b  40469  cdleme35d  40471  cdleme35e  40472  cdleme42a  40490  cdleme42ke  40504  cdlemeg46frv  40544  cdlemg2fv2  40619  cdlemg2m  40623  cdlemg10bALTN  40655  cdlemg12e  40666  cdlemg31d  40719  trlcoabs2N  40741  trlcolem  40745  trljco  40759  cdlemh2  40835  cdlemh  40836  cdlemi1  40837  cdlemk4  40853  cdlemk9  40858  cdlemk9bN  40859  cdlemkid2  40943  dia2dimlem1  41083  dia2dimlem2  41084  dia2dimlem3  41085  doca2N  41145  djajN  41156  cdlemn10  41225  dihvalcqat  41258  dih1  41305  dihglbcpreN  41319  dihmeetbclemN  41323  dihmeetlem7N  41329  dihjatc1  41330  djhlj  41420  djh01  41431  dihjatc  41436