Theorem hlol 40020

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

Syntax hints:   → wi 4   ∈ wcel 2149  OLcol 39833  OMLcoml 39834  HLchlt 40009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-iota 6489  df-fv 6541  df-ov 7411  df-oml 39838  df-hlat 40010

This theorem is referenced by:  hlop  40021  cvrexch  40079  atle  40095  athgt  40115  2at0mat0  40184  dalem24  40356  pmapjat1  40512  atmod1i1m  40517  llnexchb2lem  40527  dalawlem2  40531  dalawlem6  40535  dalawlem7  40536  dalawlem11  40540  dalawlem12  40541  poldmj1N  40587  pmapj2N  40588  2polatN  40591  lhpmcvr3  40684  lhp2at0  40691  lhp2at0nle  40694  lhpelim  40696  lhpmod2i2  40697  lhpmod6i1  40698  lhprelat3N  40699  lhple  40701  4atex2-0aOLDN  40737  trljat1  40825  trljat2  40826  cdlemc1  40850  cdlemc6  40855  cdleme0cp  40873  cdleme0cq  40874  cdleme0e  40876  cdleme1  40886  cdleme2  40887  cdleme3c  40889  cdleme4  40897  cdleme5  40899  cdleme7c  40904  cdleme7e  40906  cdleme8  40909  cdleme9  40912  cdleme10  40913  cdleme15b  40934  cdlemednpq  40958  cdleme20c  40970  cdleme20d  40971  cdleme20j  40977  cdleme22cN  41001  cdleme22d  41002  cdleme22e  41003  cdleme22eALTN  41004  cdleme23b  41009  cdleme30a  41037  cdlemefrs29pre00  41054  cdlemefrs29bpre0  41055  cdlemefrs29cpre1  41057  cdleme32fva  41096  cdleme35b  41109  cdleme35d  41111  cdleme35e  41112  cdleme42a  41130  cdleme42ke  41144  cdlemeg46frv  41184  cdlemg2fv2  41259  cdlemg2m  41263  cdlemg10bALTN  41295  cdlemg12e  41306  cdlemg31d  41359  trlcoabs2N  41381  trlcolem  41385  trljco  41399  cdlemh2  41475  cdlemh  41476  cdlemi1  41477  cdlemk4  41493  cdlemk9  41498  cdlemk9bN  41499  cdlemkid2  41583  dia2dimlem1  41723  dia2dimlem2  41724  dia2dimlem3  41725  doca2N  41785  djajN  41796  cdlemn10  41865  dihvalcqat  41898  dih1  41945  dihglbcpreN  41959  dihmeetbclemN  41963  dihmeetlem7N  41969  dihjatc1  41970  djhlj  42060  djh01  42071  dihjatc  42076