Theorem hlol 39342

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

Syntax hints:   → wi 4   ∈ wcel 2109  OLcol 39155  OMLcoml 39156  HLchlt 39331

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-oml 39160  df-hlat 39332

This theorem is referenced by:  hlop  39343  cvrexch  39402  atle  39418  athgt  39438  2at0mat0  39507  dalem24  39679  pmapjat1  39835  atmod1i1m  39840  llnexchb2lem  39850  dalawlem2  39854  dalawlem6  39858  dalawlem7  39859  dalawlem11  39863  dalawlem12  39864  poldmj1N  39910  pmapj2N  39911  2polatN  39914  lhpmcvr3  40007  lhp2at0  40014  lhp2at0nle  40017  lhpelim  40019  lhpmod2i2  40020  lhpmod6i1  40021  lhprelat3N  40022  lhple  40024  4atex2-0aOLDN  40060  trljat1  40148  trljat2  40149  cdlemc1  40173  cdlemc6  40178  cdleme0cp  40196  cdleme0cq  40197  cdleme0e  40199  cdleme1  40209  cdleme2  40210  cdleme3c  40212  cdleme4  40220  cdleme5  40222  cdleme7c  40227  cdleme7e  40229  cdleme8  40232  cdleme9  40235  cdleme10  40236  cdleme15b  40257  cdlemednpq  40281  cdleme20c  40293  cdleme20d  40294  cdleme20j  40300  cdleme22cN  40324  cdleme22d  40325  cdleme22e  40326  cdleme22eALTN  40327  cdleme23b  40332  cdleme30a  40360  cdlemefrs29pre00  40377  cdlemefrs29bpre0  40378  cdlemefrs29cpre1  40380  cdleme32fva  40419  cdleme35b  40432  cdleme35d  40434  cdleme35e  40435  cdleme42a  40453  cdleme42ke  40467  cdlemeg46frv  40507  cdlemg2fv2  40582  cdlemg2m  40586  cdlemg10bALTN  40618  cdlemg12e  40629  cdlemg31d  40682  trlcoabs2N  40704  trlcolem  40708  trljco  40722  cdlemh2  40798  cdlemh  40799  cdlemi1  40800  cdlemk4  40816  cdlemk9  40821  cdlemk9bN  40822  cdlemkid2  40906  dia2dimlem1  41046  dia2dimlem2  41047  dia2dimlem3  41048  doca2N  41108  djajN  41119  cdlemn10  41188  dihvalcqat  41221  dih1  41268  dihglbcpreN  41282  dihmeetbclemN  41286  dihmeetlem7N  41292  dihjatc1  41293  djhlj  41383  djh01  41394  dihjatc  41399