Theorem hlol 40234

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  OLcol 40047  OMLcoml 40048  HLchlt 40223

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7416  df-oml 40052  df-hlat 40224

This theorem is used by:  hlop  40235  cvrexch  40293  atle  40309  athgt  40329  2at0mat0  40398  dalem24  40570  pmapjat1  40726  atmod1i1m  40731  llnexchb2lem  40741  dalawlem2  40745  dalawlem6  40749  dalawlem7  40750  dalawlem11  40754  dalawlem12  40755  poldmj1N  40801  pmapj2N  40802  2polatN  40805  lhpmcvr3  40898  lhp2at0  40905  lhp2at0nle  40908  lhpelim  40910  lhpmod2i2  40911  lhpmod6i1  40912  lhprelat3N  40913  lhple  40915  4atex2-0aOLDN  40951  trljat1  41039  trljat2  41040  cdlemc1  41064  cdlemc6  41069  cdleme0cp  41087  cdleme0cq  41088  cdleme0e  41090  cdleme1  41100  cdleme2  41101  cdleme3c  41103  cdleme4  41111  cdleme5  41113  cdleme7c  41118  cdleme7e  41120  cdleme8  41123  cdleme9  41126  cdleme10  41127  cdleme15b  41148  cdlemednpq  41172  cdleme20c  41184  cdleme20d  41185  cdleme20j  41191  cdleme22cN  41215  cdleme22d  41216  cdleme22e  41217  cdleme22eALTN  41218  cdleme23b  41223  cdleme30a  41251  cdlemefrs29pre00  41268  cdlemefrs29bpre0  41269  cdlemefrs29cpre1  41271  cdleme32fva  41310  cdleme35b  41323  cdleme35d  41325  cdleme35e  41326  cdleme42a  41344  cdleme42ke  41358  cdlemeg46frv  41398  cdlemg2fv2  41473  cdlemg2m  41477  cdlemg10bALTN  41509  cdlemg12e  41520  cdlemg31d  41573  trlcoabs2N  41595  trlcolem  41599  trljco  41613  cdlemh2  41689  cdlemh  41690  cdlemi1  41691  cdlemk4  41707  cdlemk9  41712  cdlemk9bN  41713  cdlemkid2  41797  dia2dimlem1  41937  dia2dimlem2  41938  dia2dimlem3  41939  doca2N  41999  djajN  42010  cdlemn10  42079  dihvalcqat  42112  dih1  42159  dihglbcpreN  42173  dihmeetbclemN  42177  dihmeetlem7N  42183  dihjatc1  42184  djhlj  42274  djh01  42285  dihjatc  42290