Theorem hlol 37382

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

Syntax hints:   → wi 4   ∈ wcel 2107  OLcol 37195  OMLcoml 37196  HLchlt 37371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287  df-oml 37200  df-hlat 37372

This theorem is referenced by:  hlop  37383  cvrexch  37441  atle  37457  athgt  37477  2at0mat0  37546  dalem24  37718  pmapjat1  37874  atmod1i1m  37879  llnexchb2lem  37889  dalawlem2  37893  dalawlem6  37897  dalawlem7  37898  dalawlem11  37902  dalawlem12  37903  poldmj1N  37949  pmapj2N  37950  2polatN  37953  lhpmcvr3  38046  lhp2at0  38053  lhp2at0nle  38056  lhpelim  38058  lhpmod2i2  38059  lhpmod6i1  38060  lhprelat3N  38061  lhple  38063  4atex2-0aOLDN  38099  trljat1  38187  trljat2  38188  cdlemc1  38212  cdlemc6  38217  cdleme0cp  38235  cdleme0cq  38236  cdleme0e  38238  cdleme1  38248  cdleme2  38249  cdleme3c  38251  cdleme4  38259  cdleme5  38261  cdleme7c  38266  cdleme7e  38268  cdleme8  38271  cdleme9  38274  cdleme10  38275  cdleme15b  38296  cdlemednpq  38320  cdleme20c  38332  cdleme20d  38333  cdleme20j  38339  cdleme22cN  38363  cdleme22d  38364  cdleme22e  38365  cdleme22eALTN  38366  cdleme23b  38371  cdleme30a  38399  cdlemefrs29pre00  38416  cdlemefrs29bpre0  38417  cdlemefrs29cpre1  38419  cdleme32fva  38458  cdleme35b  38471  cdleme35d  38473  cdleme35e  38474  cdleme42a  38492  cdleme42ke  38506  cdlemeg46frv  38546  cdlemg2fv2  38621  cdlemg2m  38625  cdlemg10bALTN  38657  cdlemg12e  38668  cdlemg31d  38721  trlcoabs2N  38743  trlcolem  38747  trljco  38761  cdlemh2  38837  cdlemh  38838  cdlemi1  38839  cdlemk4  38855  cdlemk9  38860  cdlemk9bN  38861  cdlemkid2  38945  dia2dimlem1  39085  dia2dimlem2  39086  dia2dimlem3  39087  doca2N  39147  djajN  39158  cdlemn10  39227  dihvalcqat  39260  dih1  39307  dihglbcpreN  39321  dihmeetbclemN  39325  dihmeetlem7N  39331  dihjatc1  39332  djhlj  39422  djh01  39433  dihjatc  39438