Theorem hlol 35939

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

Syntax hints:   → wi 4   ∈ wcel 2050  OLcol 35752  OMLcoml 35753  HLchlt 35928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3418  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-nul 4180  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-iota 6152  df-fv 6196  df-ov 6979  df-oml 35757  df-hlat 35929

This theorem is referenced by:  hlop  35940  cvrexch  35998  atle  36014  athgt  36034  2at0mat0  36103  dalem24  36275  pmapjat1  36431  atmod1i1m  36436  llnexchb2lem  36446  dalawlem2  36450  dalawlem6  36454  dalawlem7  36455  dalawlem11  36459  dalawlem12  36460  poldmj1N  36506  pmapj2N  36507  2polatN  36510  lhpmcvr3  36603  lhp2at0  36610  lhp2at0nle  36613  lhpelim  36615  lhpmod2i2  36616  lhpmod6i1  36617  lhprelat3N  36618  lhple  36620  4atex2-0aOLDN  36656  trljat1  36744  trljat2  36745  cdlemc1  36769  cdlemc6  36774  cdleme0cp  36792  cdleme0cq  36793  cdleme0e  36795  cdleme1  36805  cdleme2  36806  cdleme3c  36808  cdleme4  36816  cdleme5  36818  cdleme7c  36823  cdleme7e  36825  cdleme8  36828  cdleme9  36831  cdleme10  36832  cdleme15b  36853  cdlemednpq  36877  cdleme20c  36889  cdleme20d  36890  cdleme20j  36896  cdleme22cN  36920  cdleme22d  36921  cdleme22e  36922  cdleme22eALTN  36923  cdleme23b  36928  cdleme30a  36956  cdlemefrs29pre00  36973  cdlemefrs29bpre0  36974  cdlemefrs29cpre1  36976  cdleme32fva  37015  cdleme35b  37028  cdleme35d  37030  cdleme35e  37031  cdleme42a  37049  cdleme42ke  37063  cdlemeg46frv  37103  cdlemg2fv2  37178  cdlemg2m  37182  cdlemg10bALTN  37214  cdlemg12e  37225  cdlemg31d  37278  trlcoabs2N  37300  trlcolem  37304  trljco  37318  cdlemh2  37394  cdlemh  37395  cdlemi1  37396  cdlemk4  37412  cdlemk9  37417  cdlemk9bN  37418  cdlemkid2  37502  dia2dimlem1  37642  dia2dimlem2  37643  dia2dimlem3  37644  doca2N  37704  djajN  37715  cdlemn10  37784  dihvalcqat  37817  dih1  37864  dihglbcpreN  37878  dihmeetbclemN  37882  dihmeetlem7N  37888  dihjatc1  37889  djhlj  37979  djh01  37990  dihjatc  37995