Theorem hlol 40116

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

Syntax hints:   → wi 4   ∈ wcel 2143  OLcol 39929  OMLcoml 39930  HLchlt 40105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-oml 39934  df-hlat 40106

This theorem is referenced by:  hlop  40117  cvrexch  40175  atle  40191  athgt  40211  2at0mat0  40280  dalem24  40452  pmapjat1  40608  atmod1i1m  40613  llnexchb2lem  40623  dalawlem2  40627  dalawlem6  40631  dalawlem7  40632  dalawlem11  40636  dalawlem12  40637  poldmj1N  40683  pmapj2N  40684  2polatN  40687  lhpmcvr3  40780  lhp2at0  40787  lhp2at0nle  40790  lhpelim  40792  lhpmod2i2  40793  lhpmod6i1  40794  lhprelat3N  40795  lhple  40797  4atex2-0aOLDN  40833  trljat1  40921  trljat2  40922  cdlemc1  40946  cdlemc6  40951  cdleme0cp  40969  cdleme0cq  40970  cdleme0e  40972  cdleme1  40982  cdleme2  40983  cdleme3c  40985  cdleme4  40993  cdleme5  40995  cdleme7c  41000  cdleme7e  41002  cdleme8  41005  cdleme9  41008  cdleme10  41009  cdleme15b  41030  cdlemednpq  41054  cdleme20c  41066  cdleme20d  41067  cdleme20j  41073  cdleme22cN  41097  cdleme22d  41098  cdleme22e  41099  cdleme22eALTN  41100  cdleme23b  41105  cdleme30a  41133  cdlemefrs29pre00  41150  cdlemefrs29bpre0  41151  cdlemefrs29cpre1  41153  cdleme32fva  41192  cdleme35b  41205  cdleme35d  41207  cdleme35e  41208  cdleme42a  41226  cdleme42ke  41240  cdlemeg46frv  41280  cdlemg2fv2  41355  cdlemg2m  41359  cdlemg10bALTN  41391  cdlemg12e  41402  cdlemg31d  41455  trlcoabs2N  41477  trlcolem  41481  trljco  41495  cdlemh2  41571  cdlemh  41572  cdlemi1  41573  cdlemk4  41589  cdlemk9  41594  cdlemk9bN  41595  cdlemkid2  41679  dia2dimlem1  41819  dia2dimlem2  41820  dia2dimlem3  41821  doca2N  41881  djajN  41892  cdlemn10  41961  dihvalcqat  41994  dih1  42041  dihglbcpreN  42055  dihmeetbclemN  42059  dihmeetlem7N  42065  dihjatc1  42066  djhlj  42156  djh01  42167  dihjatc  42172