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 2105  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 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  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