Theorem hlol 40398

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  OLcol 40211  OMLcoml 40212  HLchlt 40387

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-ov 7421  df-oml 40216  df-hlat 40388

This theorem is used by:  hlop  40399  cvrexch  40457  atle  40473  athgt  40493  2at0mat0  40562  dalem24  40734  pmapjat1  40890  atmod1i1m  40895  llnexchb2lem  40905  dalawlem2  40909  dalawlem6  40913  dalawlem7  40914  dalawlem11  40918  dalawlem12  40919  poldmj1N  40965  pmapj2N  40966  2polatN  40969  lhpmcvr3  41062  lhp2at0  41069  lhp2at0nle  41072  lhpelim  41074  lhpmod2i2  41075  lhpmod6i1  41076  lhprelat3N  41077  lhple  41079  4atex2-0aOLDN  41115  trljat1  41203  trljat2  41204  cdlemc1  41228  cdlemc6  41233  cdleme0cp  41251  cdleme0cq  41252  cdleme0e  41254  cdleme1  41264  cdleme2  41265  cdleme3c  41267  cdleme4  41275  cdleme5  41277  cdleme7c  41282  cdleme7e  41284  cdleme8  41287  cdleme9  41290  cdleme10  41291  cdleme15b  41312  cdlemednpq  41336  cdleme20c  41348  cdleme20d  41349  cdleme20j  41355  cdleme22cN  41379  cdleme22d  41380  cdleme22e  41381  cdleme22eALTN  41382  cdleme23b  41387  cdleme30a  41415  cdlemefrs29pre00  41432  cdlemefrs29bpre0  41433  cdlemefrs29cpre1  41435  cdleme32fva  41474  cdleme35b  41487  cdleme35d  41489  cdleme35e  41490  cdleme42a  41508  cdleme42ke  41522  cdlemeg46frv  41562  cdlemg2fv2  41637  cdlemg2m  41641  cdlemg10bALTN  41673  cdlemg12e  41684  cdlemg31d  41737  trlcoabs2N  41759  trlcolem  41763  trljco  41777  cdlemh2  41853  cdlemh  41854  cdlemi1  41855  cdlemk4  41871  cdlemk9  41876  cdlemk9bN  41877  cdlemkid2  41961  dia2dimlem1  42101  dia2dimlem2  42102  dia2dimlem3  42103  doca2N  42163  djajN  42174  cdlemn10  42243  dihvalcqat  42276  dih1  42323  dihglbcpreN  42337  dihmeetbclemN  42341  dihmeetlem7N  42347  dihjatc1  42348  djhlj  42438  djh01  42449  dihjatc  42454