Theorem hlol 39361

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

Syntax hints:   → wi 4   ∈ wcel 2109  OLcol 39174  OMLcoml 39175  HLchlt 39350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-oml 39179  df-hlat 39351

This theorem is referenced by:  hlop  39362  cvrexch  39421  atle  39437  athgt  39457  2at0mat0  39526  dalem24  39698  pmapjat1  39854  atmod1i1m  39859  llnexchb2lem  39869  dalawlem2  39873  dalawlem6  39877  dalawlem7  39878  dalawlem11  39882  dalawlem12  39883  poldmj1N  39929  pmapj2N  39930  2polatN  39933  lhpmcvr3  40026  lhp2at0  40033  lhp2at0nle  40036  lhpelim  40038  lhpmod2i2  40039  lhpmod6i1  40040  lhprelat3N  40041  lhple  40043  4atex2-0aOLDN  40079  trljat1  40167  trljat2  40168  cdlemc1  40192  cdlemc6  40197  cdleme0cp  40215  cdleme0cq  40216  cdleme0e  40218  cdleme1  40228  cdleme2  40229  cdleme3c  40231  cdleme4  40239  cdleme5  40241  cdleme7c  40246  cdleme7e  40248  cdleme8  40251  cdleme9  40254  cdleme10  40255  cdleme15b  40276  cdlemednpq  40300  cdleme20c  40312  cdleme20d  40313  cdleme20j  40319  cdleme22cN  40343  cdleme22d  40344  cdleme22e  40345  cdleme22eALTN  40346  cdleme23b  40351  cdleme30a  40379  cdlemefrs29pre00  40396  cdlemefrs29bpre0  40397  cdlemefrs29cpre1  40399  cdleme32fva  40438  cdleme35b  40451  cdleme35d  40453  cdleme35e  40454  cdleme42a  40472  cdleme42ke  40486  cdlemeg46frv  40526  cdlemg2fv2  40601  cdlemg2m  40605  cdlemg10bALTN  40637  cdlemg12e  40648  cdlemg31d  40701  trlcoabs2N  40723  trlcolem  40727  trljco  40741  cdlemh2  40817  cdlemh  40818  cdlemi1  40819  cdlemk4  40835  cdlemk9  40840  cdlemk9bN  40841  cdlemkid2  40925  dia2dimlem1  41065  dia2dimlem2  41066  dia2dimlem3  41067  doca2N  41127  djajN  41138  cdlemn10  41207  dihvalcqat  41240  dih1  41287  dihglbcpreN  41301  dihmeetbclemN  41305  dihmeetlem7N  41311  dihjatc1  41312  djhlj  41402  djh01  41413  dihjatc  41418