Theorem hlol 39533

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

Syntax hints:   → wi 4   ∈ wcel 2113  OLcol 39346  OMLcoml 39347  HLchlt 39522

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-oml 39351  df-hlat 39523

This theorem is referenced by:  hlop  39534  cvrexch  39592  atle  39608  athgt  39628  2at0mat0  39697  dalem24  39869  pmapjat1  40025  atmod1i1m  40030  llnexchb2lem  40040  dalawlem2  40044  dalawlem6  40048  dalawlem7  40049  dalawlem11  40053  dalawlem12  40054  poldmj1N  40100  pmapj2N  40101  2polatN  40104  lhpmcvr3  40197  lhp2at0  40204  lhp2at0nle  40207  lhpelim  40209  lhpmod2i2  40210  lhpmod6i1  40211  lhprelat3N  40212  lhple  40214  4atex2-0aOLDN  40250  trljat1  40338  trljat2  40339  cdlemc1  40363  cdlemc6  40368  cdleme0cp  40386  cdleme0cq  40387  cdleme0e  40389  cdleme1  40399  cdleme2  40400  cdleme3c  40402  cdleme4  40410  cdleme5  40412  cdleme7c  40417  cdleme7e  40419  cdleme8  40422  cdleme9  40425  cdleme10  40426  cdleme15b  40447  cdlemednpq  40471  cdleme20c  40483  cdleme20d  40484  cdleme20j  40490  cdleme22cN  40514  cdleme22d  40515  cdleme22e  40516  cdleme22eALTN  40517  cdleme23b  40522  cdleme30a  40550  cdlemefrs29pre00  40567  cdlemefrs29bpre0  40568  cdlemefrs29cpre1  40570  cdleme32fva  40609  cdleme35b  40622  cdleme35d  40624  cdleme35e  40625  cdleme42a  40643  cdleme42ke  40657  cdlemeg46frv  40697  cdlemg2fv2  40772  cdlemg2m  40776  cdlemg10bALTN  40808  cdlemg12e  40819  cdlemg31d  40872  trlcoabs2N  40894  trlcolem  40898  trljco  40912  cdlemh2  40988  cdlemh  40989  cdlemi1  40990  cdlemk4  41006  cdlemk9  41011  cdlemk9bN  41012  cdlemkid2  41096  dia2dimlem1  41236  dia2dimlem2  41237  dia2dimlem3  41238  doca2N  41298  djajN  41309  cdlemn10  41378  dihvalcqat  41411  dih1  41458  dihglbcpreN  41472  dihmeetbclemN  41476  dihmeetlem7N  41482  dihjatc1  41483  djhlj  41573  djh01  41584  dihjatc  41589