Theorem hlol 36657

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

Syntax hints:   → wi 4   ∈ wcel 2111  OLcol 36470  OMLcoml 36471  HLchlt 36646

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-oml 36475  df-hlat 36647

This theorem is referenced by:  hlop  36658  cvrexch  36716  atle  36732  athgt  36752  2at0mat0  36821  dalem24  36993  pmapjat1  37149  atmod1i1m  37154  llnexchb2lem  37164  dalawlem2  37168  dalawlem6  37172  dalawlem7  37173  dalawlem11  37177  dalawlem12  37178  poldmj1N  37224  pmapj2N  37225  2polatN  37228  lhpmcvr3  37321  lhp2at0  37328  lhp2at0nle  37331  lhpelim  37333  lhpmod2i2  37334  lhpmod6i1  37335  lhprelat3N  37336  lhple  37338  4atex2-0aOLDN  37374  trljat1  37462  trljat2  37463  cdlemc1  37487  cdlemc6  37492  cdleme0cp  37510  cdleme0cq  37511  cdleme0e  37513  cdleme1  37523  cdleme2  37524  cdleme3c  37526  cdleme4  37534  cdleme5  37536  cdleme7c  37541  cdleme7e  37543  cdleme8  37546  cdleme9  37549  cdleme10  37550  cdleme15b  37571  cdlemednpq  37595  cdleme20c  37607  cdleme20d  37608  cdleme20j  37614  cdleme22cN  37638  cdleme22d  37639  cdleme22e  37640  cdleme22eALTN  37641  cdleme23b  37646  cdleme30a  37674  cdlemefrs29pre00  37691  cdlemefrs29bpre0  37692  cdlemefrs29cpre1  37694  cdleme32fva  37733  cdleme35b  37746  cdleme35d  37748  cdleme35e  37749  cdleme42a  37767  cdleme42ke  37781  cdlemeg46frv  37821  cdlemg2fv2  37896  cdlemg2m  37900  cdlemg10bALTN  37932  cdlemg12e  37943  cdlemg31d  37996  trlcoabs2N  38018  trlcolem  38022  trljco  38036  cdlemh2  38112  cdlemh  38113  cdlemi1  38114  cdlemk4  38130  cdlemk9  38135  cdlemk9bN  38136  cdlemkid2  38220  dia2dimlem1  38360  dia2dimlem2  38361  dia2dimlem3  38362  doca2N  38422  djajN  38433  cdlemn10  38502  dihvalcqat  38535  dih1  38582  dihglbcpreN  38596  dihmeetbclemN  38600  dihmeetlem7N  38606  dihjatc1  38607  djhlj  38697  djh01  38708  dihjatc  38713