Theorem hlol 36499

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

Syntax hints:   → wi 4   ∈ wcel 2114  OLcol 36312  OMLcoml 36313  HLchlt 36488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161  df-oml 36317  df-hlat 36489

This theorem is referenced by:  hlop  36500  cvrexch  36558  atle  36574  athgt  36594  2at0mat0  36663  dalem24  36835  pmapjat1  36991  atmod1i1m  36996  llnexchb2lem  37006  dalawlem2  37010  dalawlem6  37014  dalawlem7  37015  dalawlem11  37019  dalawlem12  37020  poldmj1N  37066  pmapj2N  37067  2polatN  37070  lhpmcvr3  37163  lhp2at0  37170  lhp2at0nle  37173  lhpelim  37175  lhpmod2i2  37176  lhpmod6i1  37177  lhprelat3N  37178  lhple  37180  4atex2-0aOLDN  37216  trljat1  37304  trljat2  37305  cdlemc1  37329  cdlemc6  37334  cdleme0cp  37352  cdleme0cq  37353  cdleme0e  37355  cdleme1  37365  cdleme2  37366  cdleme3c  37368  cdleme4  37376  cdleme5  37378  cdleme7c  37383  cdleme7e  37385  cdleme8  37388  cdleme9  37391  cdleme10  37392  cdleme15b  37413  cdlemednpq  37437  cdleme20c  37449  cdleme20d  37450  cdleme20j  37456  cdleme22cN  37480  cdleme22d  37481  cdleme22e  37482  cdleme22eALTN  37483  cdleme23b  37488  cdleme30a  37516  cdlemefrs29pre00  37533  cdlemefrs29bpre0  37534  cdlemefrs29cpre1  37536  cdleme32fva  37575  cdleme35b  37588  cdleme35d  37590  cdleme35e  37591  cdleme42a  37609  cdleme42ke  37623  cdlemeg46frv  37663  cdlemg2fv2  37738  cdlemg2m  37742  cdlemg10bALTN  37774  cdlemg12e  37785  cdlemg31d  37838  trlcoabs2N  37860  trlcolem  37864  trljco  37878  cdlemh2  37954  cdlemh  37955  cdlemi1  37956  cdlemk4  37972  cdlemk9  37977  cdlemk9bN  37978  cdlemkid2  38062  dia2dimlem1  38202  dia2dimlem2  38203  dia2dimlem3  38204  doca2N  38264  djajN  38275  cdlemn10  38344  dihvalcqat  38377  dih1  38424  dihglbcpreN  38438  dihmeetbclemN  38442  dihmeetlem7N  38448  dihjatc1  38449  djhlj  38539  djh01  38550  dihjatc  38555