Theorem hlol 35169

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

Syntax hints:   → wi 4   ∈ wcel 2145  OLcol 34982  OMLcoml 34983  HLchlt 35158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-iota 5993  df-fv 6038  df-ov 6798  df-oml 34987  df-hlat 35159

This theorem is referenced by:  hlop  35170  cvrexch  35228  atle  35244  athgt  35264  2at0mat0  35333  dalem24  35505  pmapjat1  35661  atmod1i1m  35666  llnexchb2lem  35676  dalawlem2  35680  dalawlem6  35684  dalawlem7  35685  dalawlem11  35689  dalawlem12  35690  poldmj1N  35736  pmapj2N  35737  2polatN  35740  lhpmcvr3  35833  lhp2at0  35840  lhp2at0nle  35843  lhpelim  35845  lhpmod2i2  35846  lhpmod6i1  35847  lhprelat3N  35848  lhple  35850  4atex2-0aOLDN  35886  trljat1  35975  trljat2  35976  cdlemc1  36000  cdlemc6  36005  cdleme0cp  36023  cdleme0cq  36024  cdleme0e  36026  cdleme1  36036  cdleme2  36037  cdleme3c  36039  cdleme4  36047  cdleme5  36049  cdleme7c  36054  cdleme7e  36056  cdleme8  36059  cdleme9  36062  cdleme10  36063  cdleme15b  36084  cdlemednpq  36108  cdleme20c  36120  cdleme20d  36121  cdleme20j  36127  cdleme22cN  36151  cdleme22d  36152  cdleme22e  36153  cdleme22eALTN  36154  cdleme23b  36159  cdleme30a  36187  cdlemefrs29pre00  36204  cdlemefrs29bpre0  36205  cdlemefrs29cpre1  36207  cdleme32fva  36246  cdleme35b  36259  cdleme35d  36261  cdleme35e  36262  cdleme42a  36280  cdleme42ke  36294  cdlemeg46frv  36334  cdlemg2fv2  36409  cdlemg2m  36413  cdlemg10bALTN  36445  cdlemg12e  36456  cdlemg31d  36509  trlcoabs2N  36531  trlcolem  36535  trljco  36549  cdlemh2  36625  cdlemh  36626  cdlemi1  36627  cdlemk4  36643  cdlemk9  36648  cdlemk9bN  36649  cdlemkid2  36733  dia2dimlem1  36874  dia2dimlem2  36875  dia2dimlem3  36876  doca2N  36936  djajN  36947  cdlemn10  37016  dihvalcqat  37049  dih1  37096  dihglbcpreN  37110  dihmeetbclemN  37114  dihmeetlem7N  37120  dihjatc1  37121  djhlj  37211  djh01  37222  dihjatc  37227