Theorem hlol 39798

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

Syntax hints:   → wi 4   ∈ wcel 2114  OLcol 39611  OMLcoml 39612  HLchlt 39787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361  df-oml 39616  df-hlat 39788

This theorem is referenced by:  hlop  39799  cvrexch  39857  atle  39873  athgt  39893  2at0mat0  39962  dalem24  40134  pmapjat1  40290  atmod1i1m  40295  llnexchb2lem  40305  dalawlem2  40309  dalawlem6  40313  dalawlem7  40314  dalawlem11  40318  dalawlem12  40319  poldmj1N  40365  pmapj2N  40366  2polatN  40369  lhpmcvr3  40462  lhp2at0  40469  lhp2at0nle  40472  lhpelim  40474  lhpmod2i2  40475  lhpmod6i1  40476  lhprelat3N  40477  lhple  40479  4atex2-0aOLDN  40515  trljat1  40603  trljat2  40604  cdlemc1  40628  cdlemc6  40633  cdleme0cp  40651  cdleme0cq  40652  cdleme0e  40654  cdleme1  40664  cdleme2  40665  cdleme3c  40667  cdleme4  40675  cdleme5  40677  cdleme7c  40682  cdleme7e  40684  cdleme8  40687  cdleme9  40690  cdleme10  40691  cdleme15b  40712  cdlemednpq  40736  cdleme20c  40748  cdleme20d  40749  cdleme20j  40755  cdleme22cN  40779  cdleme22d  40780  cdleme22e  40781  cdleme22eALTN  40782  cdleme23b  40787  cdleme30a  40815  cdlemefrs29pre00  40832  cdlemefrs29bpre0  40833  cdlemefrs29cpre1  40835  cdleme32fva  40874  cdleme35b  40887  cdleme35d  40889  cdleme35e  40890  cdleme42a  40908  cdleme42ke  40922  cdlemeg46frv  40962  cdlemg2fv2  41037  cdlemg2m  41041  cdlemg10bALTN  41073  cdlemg12e  41084  cdlemg31d  41137  trlcoabs2N  41159  trlcolem  41163  trljco  41177  cdlemh2  41253  cdlemh  41254  cdlemi1  41255  cdlemk4  41271  cdlemk9  41276  cdlemk9bN  41277  cdlemkid2  41361  dia2dimlem1  41501  dia2dimlem2  41502  dia2dimlem3  41503  doca2N  41563  djajN  41574  cdlemn10  41643  dihvalcqat  41676  dih1  41723  dihglbcpreN  41737  dihmeetbclemN  41741  dihmeetlem7N  41747  dihjatc1  41748  djhlj  41838  djh01  41849  dihjatc  41854