Theorem hlol 39621

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

Syntax hints:   → wi 4   ∈ wcel 2113  OLcol 39434  OMLcoml 39435  HLchlt 39610

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-oml 39439  df-hlat 39611

This theorem is referenced by:  hlop  39622  cvrexch  39680  atle  39696  athgt  39716  2at0mat0  39785  dalem24  39957  pmapjat1  40113  atmod1i1m  40118  llnexchb2lem  40128  dalawlem2  40132  dalawlem6  40136  dalawlem7  40137  dalawlem11  40141  dalawlem12  40142  poldmj1N  40188  pmapj2N  40189  2polatN  40192  lhpmcvr3  40285  lhp2at0  40292  lhp2at0nle  40295  lhpelim  40297  lhpmod2i2  40298  lhpmod6i1  40299  lhprelat3N  40300  lhple  40302  4atex2-0aOLDN  40338  trljat1  40426  trljat2  40427  cdlemc1  40451  cdlemc6  40456  cdleme0cp  40474  cdleme0cq  40475  cdleme0e  40477  cdleme1  40487  cdleme2  40488  cdleme3c  40490  cdleme4  40498  cdleme5  40500  cdleme7c  40505  cdleme7e  40507  cdleme8  40510  cdleme9  40513  cdleme10  40514  cdleme15b  40535  cdlemednpq  40559  cdleme20c  40571  cdleme20d  40572  cdleme20j  40578  cdleme22cN  40602  cdleme22d  40603  cdleme22e  40604  cdleme22eALTN  40605  cdleme23b  40610  cdleme30a  40638  cdlemefrs29pre00  40655  cdlemefrs29bpre0  40656  cdlemefrs29cpre1  40658  cdleme32fva  40697  cdleme35b  40710  cdleme35d  40712  cdleme35e  40713  cdleme42a  40731  cdleme42ke  40745  cdlemeg46frv  40785  cdlemg2fv2  40860  cdlemg2m  40864  cdlemg10bALTN  40896  cdlemg12e  40907  cdlemg31d  40960  trlcoabs2N  40982  trlcolem  40986  trljco  41000  cdlemh2  41076  cdlemh  41077  cdlemi1  41078  cdlemk4  41094  cdlemk9  41099  cdlemk9bN  41100  cdlemkid2  41184  dia2dimlem1  41324  dia2dimlem2  41325  dia2dimlem3  41326  doca2N  41386  djajN  41397  cdlemn10  41466  dihvalcqat  41499  dih1  41546  dihglbcpreN  41560  dihmeetbclemN  41564  dihmeetlem7N  41570  dihjatc1  41571  djhlj  41661  djh01  41672  dihjatc  41677