Theorem hlol 39400

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

Syntax hints:   → wi 4   ∈ wcel 2111  OLcol 39213  OMLcoml 39214  HLchlt 39389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-iota 6432  df-fv 6484  df-ov 7344  df-oml 39218  df-hlat 39390

This theorem is referenced by:  hlop  39401  cvrexch  39459  atle  39475  athgt  39495  2at0mat0  39564  dalem24  39736  pmapjat1  39892  atmod1i1m  39897  llnexchb2lem  39907  dalawlem2  39911  dalawlem6  39915  dalawlem7  39916  dalawlem11  39920  dalawlem12  39921  poldmj1N  39967  pmapj2N  39968  2polatN  39971  lhpmcvr3  40064  lhp2at0  40071  lhp2at0nle  40074  lhpelim  40076  lhpmod2i2  40077  lhpmod6i1  40078  lhprelat3N  40079  lhple  40081  4atex2-0aOLDN  40117  trljat1  40205  trljat2  40206  cdlemc1  40230  cdlemc6  40235  cdleme0cp  40253  cdleme0cq  40254  cdleme0e  40256  cdleme1  40266  cdleme2  40267  cdleme3c  40269  cdleme4  40277  cdleme5  40279  cdleme7c  40284  cdleme7e  40286  cdleme8  40289  cdleme9  40292  cdleme10  40293  cdleme15b  40314  cdlemednpq  40338  cdleme20c  40350  cdleme20d  40351  cdleme20j  40357  cdleme22cN  40381  cdleme22d  40382  cdleme22e  40383  cdleme22eALTN  40384  cdleme23b  40389  cdleme30a  40417  cdlemefrs29pre00  40434  cdlemefrs29bpre0  40435  cdlemefrs29cpre1  40437  cdleme32fva  40476  cdleme35b  40489  cdleme35d  40491  cdleme35e  40492  cdleme42a  40510  cdleme42ke  40524  cdlemeg46frv  40564  cdlemg2fv2  40639  cdlemg2m  40643  cdlemg10bALTN  40675  cdlemg12e  40686  cdlemg31d  40739  trlcoabs2N  40761  trlcolem  40765  trljco  40779  cdlemh2  40855  cdlemh  40856  cdlemi1  40857  cdlemk4  40873  cdlemk9  40878  cdlemk9bN  40879  cdlemkid2  40963  dia2dimlem1  41103  dia2dimlem2  41104  dia2dimlem3  41105  doca2N  41165  djajN  41176  cdlemn10  41245  dihvalcqat  41278  dih1  41325  dihglbcpreN  41339  dihmeetbclemN  41343  dihmeetlem7N  41349  dihjatc1  41350  djhlj  41440  djh01  41451  dihjatc  41456