Theorem hlol 36512

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

Syntax hints:   → wi 4   ∈ wcel 2114  OLcol 36325  OMLcoml 36326  HLchlt 36501

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-oml 36330  df-hlat 36502

This theorem is referenced by:  hlop  36513  cvrexch  36571  atle  36587  athgt  36607  2at0mat0  36676  dalem24  36848  pmapjat1  37004  atmod1i1m  37009  llnexchb2lem  37019  dalawlem2  37023  dalawlem6  37027  dalawlem7  37028  dalawlem11  37032  dalawlem12  37033  poldmj1N  37079  pmapj2N  37080  2polatN  37083  lhpmcvr3  37176  lhp2at0  37183  lhp2at0nle  37186  lhpelim  37188  lhpmod2i2  37189  lhpmod6i1  37190  lhprelat3N  37191  lhple  37193  4atex2-0aOLDN  37229  trljat1  37317  trljat2  37318  cdlemc1  37342  cdlemc6  37347  cdleme0cp  37365  cdleme0cq  37366  cdleme0e  37368  cdleme1  37378  cdleme2  37379  cdleme3c  37381  cdleme4  37389  cdleme5  37391  cdleme7c  37396  cdleme7e  37398  cdleme8  37401  cdleme9  37404  cdleme10  37405  cdleme15b  37426  cdlemednpq  37450  cdleme20c  37462  cdleme20d  37463  cdleme20j  37469  cdleme22cN  37493  cdleme22d  37494  cdleme22e  37495  cdleme22eALTN  37496  cdleme23b  37501  cdleme30a  37529  cdlemefrs29pre00  37546  cdlemefrs29bpre0  37547  cdlemefrs29cpre1  37549  cdleme32fva  37588  cdleme35b  37601  cdleme35d  37603  cdleme35e  37604  cdleme42a  37622  cdleme42ke  37636  cdlemeg46frv  37676  cdlemg2fv2  37751  cdlemg2m  37755  cdlemg10bALTN  37787  cdlemg12e  37798  cdlemg31d  37851  trlcoabs2N  37873  trlcolem  37877  trljco  37891  cdlemh2  37967  cdlemh  37968  cdlemi1  37969  cdlemk4  37985  cdlemk9  37990  cdlemk9bN  37991  cdlemkid2  38075  dia2dimlem1  38215  dia2dimlem2  38216  dia2dimlem3  38217  doca2N  38277  djajN  38288  cdlemn10  38357  dihvalcqat  38390  dih1  38437  dihglbcpreN  38451  dihmeetbclemN  38455  dihmeetlem7N  38461  dihjatc1  38462  djhlj  38552  djh01  38563  dihjatc  38568