Theorem hlol 39853

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

Syntax hints:   → wi 4   ∈ wcel 2119  OLcol 39666  OMLcoml 39667  HLchlt 39842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-oml 39671  df-hlat 39843

This theorem is referenced by:  hlop  39854  cvrexch  39912  atle  39928  athgt  39948  2at0mat0  40017  dalem24  40189  pmapjat1  40345  atmod1i1m  40350  llnexchb2lem  40360  dalawlem2  40364  dalawlem6  40368  dalawlem7  40369  dalawlem11  40373  dalawlem12  40374  poldmj1N  40420  pmapj2N  40421  2polatN  40424  lhpmcvr3  40517  lhp2at0  40524  lhp2at0nle  40527  lhpelim  40529  lhpmod2i2  40530  lhpmod6i1  40531  lhprelat3N  40532  lhple  40534  4atex2-0aOLDN  40570  trljat1  40658  trljat2  40659  cdlemc1  40683  cdlemc6  40688  cdleme0cp  40706  cdleme0cq  40707  cdleme0e  40709  cdleme1  40719  cdleme2  40720  cdleme3c  40722  cdleme4  40730  cdleme5  40732  cdleme7c  40737  cdleme7e  40739  cdleme8  40742  cdleme9  40745  cdleme10  40746  cdleme15b  40767  cdlemednpq  40791  cdleme20c  40803  cdleme20d  40804  cdleme20j  40810  cdleme22cN  40834  cdleme22d  40835  cdleme22e  40836  cdleme22eALTN  40837  cdleme23b  40842  cdleme30a  40870  cdlemefrs29pre00  40887  cdlemefrs29bpre0  40888  cdlemefrs29cpre1  40890  cdleme32fva  40929  cdleme35b  40942  cdleme35d  40944  cdleme35e  40945  cdleme42a  40963  cdleme42ke  40977  cdlemeg46frv  41017  cdlemg2fv2  41092  cdlemg2m  41096  cdlemg10bALTN  41128  cdlemg12e  41139  cdlemg31d  41192  trlcoabs2N  41214  trlcolem  41218  trljco  41232  cdlemh2  41308  cdlemh  41309  cdlemi1  41310  cdlemk4  41326  cdlemk9  41331  cdlemk9bN  41332  cdlemkid2  41416  dia2dimlem1  41556  dia2dimlem2  41557  dia2dimlem3  41558  doca2N  41618  djajN  41629  cdlemn10  41698  dihvalcqat  41731  dih1  41778  dihglbcpreN  41792  dihmeetbclemN  41796  dihmeetlem7N  41802  dihjatc1  41803  djhlj  41893  djh01  41904  dihjatc  41909