Theorem hlol 39327

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

Syntax hints:   → wi 4   ∈ wcel 2109  OLcol 39140  OMLcoml 39141  HLchlt 39316

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-oml 39145  df-hlat 39317

This theorem is referenced by:  hlop  39328  cvrexch  39387  atle  39403  athgt  39423  2at0mat0  39492  dalem24  39664  pmapjat1  39820  atmod1i1m  39825  llnexchb2lem  39835  dalawlem2  39839  dalawlem6  39843  dalawlem7  39844  dalawlem11  39848  dalawlem12  39849  poldmj1N  39895  pmapj2N  39896  2polatN  39899  lhpmcvr3  39992  lhp2at0  39999  lhp2at0nle  40002  lhpelim  40004  lhpmod2i2  40005  lhpmod6i1  40006  lhprelat3N  40007  lhple  40009  4atex2-0aOLDN  40045  trljat1  40133  trljat2  40134  cdlemc1  40158  cdlemc6  40163  cdleme0cp  40181  cdleme0cq  40182  cdleme0e  40184  cdleme1  40194  cdleme2  40195  cdleme3c  40197  cdleme4  40205  cdleme5  40207  cdleme7c  40212  cdleme7e  40214  cdleme8  40217  cdleme9  40220  cdleme10  40221  cdleme15b  40242  cdlemednpq  40266  cdleme20c  40278  cdleme20d  40279  cdleme20j  40285  cdleme22cN  40309  cdleme22d  40310  cdleme22e  40311  cdleme22eALTN  40312  cdleme23b  40317  cdleme30a  40345  cdlemefrs29pre00  40362  cdlemefrs29bpre0  40363  cdlemefrs29cpre1  40365  cdleme32fva  40404  cdleme35b  40417  cdleme35d  40419  cdleme35e  40420  cdleme42a  40438  cdleme42ke  40452  cdlemeg46frv  40492  cdlemg2fv2  40567  cdlemg2m  40571  cdlemg10bALTN  40603  cdlemg12e  40614  cdlemg31d  40667  trlcoabs2N  40689  trlcolem  40693  trljco  40707  cdlemh2  40783  cdlemh  40784  cdlemi1  40785  cdlemk4  40801  cdlemk9  40806  cdlemk9bN  40807  cdlemkid2  40891  dia2dimlem1  41031  dia2dimlem2  41032  dia2dimlem3  41033  doca2N  41093  djajN  41104  cdlemn10  41173  dihvalcqat  41206  dih1  41253  dihglbcpreN  41267  dihmeetbclemN  41271  dihmeetlem7N  41277  dihjatc1  41278  djhlj  41368  djh01  41379  dihjatc  41384