Theorem hlol 39354

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

Syntax hints:   → wi 4   ∈ wcel 2109  OLcol 39167  OMLcoml 39168  HLchlt 39343

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-oml 39172  df-hlat 39344

This theorem is referenced by:  hlop  39355  cvrexch  39414  atle  39430  athgt  39450  2at0mat0  39519  dalem24  39691  pmapjat1  39847  atmod1i1m  39852  llnexchb2lem  39862  dalawlem2  39866  dalawlem6  39870  dalawlem7  39871  dalawlem11  39875  dalawlem12  39876  poldmj1N  39922  pmapj2N  39923  2polatN  39926  lhpmcvr3  40019  lhp2at0  40026  lhp2at0nle  40029  lhpelim  40031  lhpmod2i2  40032  lhpmod6i1  40033  lhprelat3N  40034  lhple  40036  4atex2-0aOLDN  40072  trljat1  40160  trljat2  40161  cdlemc1  40185  cdlemc6  40190  cdleme0cp  40208  cdleme0cq  40209  cdleme0e  40211  cdleme1  40221  cdleme2  40222  cdleme3c  40224  cdleme4  40232  cdleme5  40234  cdleme7c  40239  cdleme7e  40241  cdleme8  40244  cdleme9  40247  cdleme10  40248  cdleme15b  40269  cdlemednpq  40293  cdleme20c  40305  cdleme20d  40306  cdleme20j  40312  cdleme22cN  40336  cdleme22d  40337  cdleme22e  40338  cdleme22eALTN  40339  cdleme23b  40344  cdleme30a  40372  cdlemefrs29pre00  40389  cdlemefrs29bpre0  40390  cdlemefrs29cpre1  40392  cdleme32fva  40431  cdleme35b  40444  cdleme35d  40446  cdleme35e  40447  cdleme42a  40465  cdleme42ke  40479  cdlemeg46frv  40519  cdlemg2fv2  40594  cdlemg2m  40598  cdlemg10bALTN  40630  cdlemg12e  40641  cdlemg31d  40694  trlcoabs2N  40716  trlcolem  40720  trljco  40734  cdlemh2  40810  cdlemh  40811  cdlemi1  40812  cdlemk4  40828  cdlemk9  40833  cdlemk9bN  40834  cdlemkid2  40918  dia2dimlem1  41058  dia2dimlem2  41059  dia2dimlem3  41060  doca2N  41120  djajN  41131  cdlemn10  41200  dihvalcqat  41233  dih1  41280  dihglbcpreN  41294  dihmeetbclemN  41298  dihmeetlem7N  41304  dihjatc1  41305  djhlj  41395  djh01  41406  dihjatc  41411