Theorem hlol 39946

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

Syntax hints:   → wi 4   ∈ wcel 2141  OLcol 39759  OMLcoml 39760  HLchlt 39935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524  df-ov 7394  df-oml 39764  df-hlat 39936

This theorem is referenced by:  hlop  39947  cvrexch  40005  atle  40021  athgt  40041  2at0mat0  40110  dalem24  40282  pmapjat1  40438  atmod1i1m  40443  llnexchb2lem  40453  dalawlem2  40457  dalawlem6  40461  dalawlem7  40462  dalawlem11  40466  dalawlem12  40467  poldmj1N  40513  pmapj2N  40514  2polatN  40517  lhpmcvr3  40610  lhp2at0  40617  lhp2at0nle  40620  lhpelim  40622  lhpmod2i2  40623  lhpmod6i1  40624  lhprelat3N  40625  lhple  40627  4atex2-0aOLDN  40663  trljat1  40751  trljat2  40752  cdlemc1  40776  cdlemc6  40781  cdleme0cp  40799  cdleme0cq  40800  cdleme0e  40802  cdleme1  40812  cdleme2  40813  cdleme3c  40815  cdleme4  40823  cdleme5  40825  cdleme7c  40830  cdleme7e  40832  cdleme8  40835  cdleme9  40838  cdleme10  40839  cdleme15b  40860  cdlemednpq  40884  cdleme20c  40896  cdleme20d  40897  cdleme20j  40903  cdleme22cN  40927  cdleme22d  40928  cdleme22e  40929  cdleme22eALTN  40930  cdleme23b  40935  cdleme30a  40963  cdlemefrs29pre00  40980  cdlemefrs29bpre0  40981  cdlemefrs29cpre1  40983  cdleme32fva  41022  cdleme35b  41035  cdleme35d  41037  cdleme35e  41038  cdleme42a  41056  cdleme42ke  41070  cdlemeg46frv  41110  cdlemg2fv2  41185  cdlemg2m  41189  cdlemg10bALTN  41221  cdlemg12e  41232  cdlemg31d  41285  trlcoabs2N  41307  trlcolem  41311  trljco  41325  cdlemh2  41401  cdlemh  41402  cdlemi1  41403  cdlemk4  41419  cdlemk9  41424  cdlemk9bN  41425  cdlemkid2  41509  dia2dimlem1  41649  dia2dimlem2  41650  dia2dimlem3  41651  doca2N  41711  djajN  41722  cdlemn10  41791  dihvalcqat  41824  dih1  41871  dihglbcpreN  41885  dihmeetbclemN  41889  dihmeetlem7N  41895  dihjatc1  41896  djhlj  41986  djh01  41997  dihjatc  42002