Theorem hlol 39807

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

Syntax hints:   → wi 4   ∈ wcel 2114  OLcol 39620  OMLcoml 39621  HLchlt 39796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-oml 39625  df-hlat 39797

This theorem is referenced by:  hlop  39808  cvrexch  39866  atle  39882  athgt  39902  2at0mat0  39971  dalem24  40143  pmapjat1  40299  atmod1i1m  40304  llnexchb2lem  40314  dalawlem2  40318  dalawlem6  40322  dalawlem7  40323  dalawlem11  40327  dalawlem12  40328  poldmj1N  40374  pmapj2N  40375  2polatN  40378  lhpmcvr3  40471  lhp2at0  40478  lhp2at0nle  40481  lhpelim  40483  lhpmod2i2  40484  lhpmod6i1  40485  lhprelat3N  40486  lhple  40488  4atex2-0aOLDN  40524  trljat1  40612  trljat2  40613  cdlemc1  40637  cdlemc6  40642  cdleme0cp  40660  cdleme0cq  40661  cdleme0e  40663  cdleme1  40673  cdleme2  40674  cdleme3c  40676  cdleme4  40684  cdleme5  40686  cdleme7c  40691  cdleme7e  40693  cdleme8  40696  cdleme9  40699  cdleme10  40700  cdleme15b  40721  cdlemednpq  40745  cdleme20c  40757  cdleme20d  40758  cdleme20j  40764  cdleme22cN  40788  cdleme22d  40789  cdleme22e  40790  cdleme22eALTN  40791  cdleme23b  40796  cdleme30a  40824  cdlemefrs29pre00  40841  cdlemefrs29bpre0  40842  cdlemefrs29cpre1  40844  cdleme32fva  40883  cdleme35b  40896  cdleme35d  40898  cdleme35e  40899  cdleme42a  40917  cdleme42ke  40931  cdlemeg46frv  40971  cdlemg2fv2  41046  cdlemg2m  41050  cdlemg10bALTN  41082  cdlemg12e  41093  cdlemg31d  41146  trlcoabs2N  41168  trlcolem  41172  trljco  41186  cdlemh2  41262  cdlemh  41263  cdlemi1  41264  cdlemk4  41280  cdlemk9  41285  cdlemk9bN  41286  cdlemkid2  41370  dia2dimlem1  41510  dia2dimlem2  41511  dia2dimlem3  41512  doca2N  41572  djajN  41583  cdlemn10  41652  dihvalcqat  41685  dih1  41732  dihglbcpreN  41746  dihmeetbclemN  41750  dihmeetlem7N  41756  dihjatc1  41757  djhlj  41847  djh01  41858  dihjatc  41863