Theorem hlol 40168

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  OLcol 39981  OMLcoml 39982  HLchlt 40157

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7419  df-oml 39986  df-hlat 40158

This theorem is used by:  hlop  40169  cvrexch  40227  atle  40243  athgt  40263  2at0mat0  40332  dalem24  40504  pmapjat1  40660  atmod1i1m  40665  llnexchb2lem  40675  dalawlem2  40679  dalawlem6  40683  dalawlem7  40684  dalawlem11  40688  dalawlem12  40689  poldmj1N  40735  pmapj2N  40736  2polatN  40739  lhpmcvr3  40832  lhp2at0  40839  lhp2at0nle  40842  lhpelim  40844  lhpmod2i2  40845  lhpmod6i1  40846  lhprelat3N  40847  lhple  40849  4atex2-0aOLDN  40885  trljat1  40973  trljat2  40974  cdlemc1  40998  cdlemc6  41003  cdleme0cp  41021  cdleme0cq  41022  cdleme0e  41024  cdleme1  41034  cdleme2  41035  cdleme3c  41037  cdleme4  41045  cdleme5  41047  cdleme7c  41052  cdleme7e  41054  cdleme8  41057  cdleme9  41060  cdleme10  41061  cdleme15b  41082  cdlemednpq  41106  cdleme20c  41118  cdleme20d  41119  cdleme20j  41125  cdleme22cN  41149  cdleme22d  41150  cdleme22e  41151  cdleme22eALTN  41152  cdleme23b  41157  cdleme30a  41185  cdlemefrs29pre00  41202  cdlemefrs29bpre0  41203  cdlemefrs29cpre1  41205  cdleme32fva  41244  cdleme35b  41257  cdleme35d  41259  cdleme35e  41260  cdleme42a  41278  cdleme42ke  41292  cdlemeg46frv  41332  cdlemg2fv2  41407  cdlemg2m  41411  cdlemg10bALTN  41443  cdlemg12e  41454  cdlemg31d  41507  trlcoabs2N  41529  trlcolem  41533  trljco  41547  cdlemh2  41623  cdlemh  41624  cdlemi1  41625  cdlemk4  41641  cdlemk9  41646  cdlemk9bN  41647  cdlemkid2  41731  dia2dimlem1  41871  dia2dimlem2  41872  dia2dimlem3  41873  doca2N  41933  djajN  41944  cdlemn10  42013  dihvalcqat  42046  dih1  42093  dihglbcpreN  42107  dihmeetbclemN  42111  dihmeetlem7N  42117  dihjatc1  42118  djhlj  42208  djh01  42219  dihjatc  42224