Theorem hlol 40684

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  OLcol 40497  OMLcoml 40498  HLchlt 40673

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-oml 40502  df-hlat 40674

This theorem is used by:  hlop  40685  cvrexch  40743  atle  40759  athgt  40779  2at0mat0  40848  dalem24  41020  pmapjat1  41176  atmod1i1m  41181  llnexchb2lem  41191  dalawlem2  41195  dalawlem6  41199  dalawlem7  41200  dalawlem11  41204  dalawlem12  41205  poldmj1N  41251  pmapj2N  41252  2polatN  41255  lhpmcvr3  41348  lhp2at0  41355  lhp2at0nle  41358  lhpelim  41360  lhpmod2i2  41361  lhpmod6i1  41362  lhprelat3N  41363  lhple  41365  4atex2-0aOLDN  41401  trljat1  41489  trljat2  41490  cdlemc1  41514  cdlemc6  41519  cdleme0cp  41537  cdleme0cq  41538  cdleme0e  41540  cdleme1  41550  cdleme2  41551  cdleme3c  41553  cdleme4  41561  cdleme5  41563  cdleme7c  41568  cdleme7e  41570  cdleme8  41573  cdleme9  41576  cdleme10  41577  cdleme15b  41598  cdlemednpq  41622  cdleme20c  41634  cdleme20d  41635  cdleme20j  41641  cdleme22cN  41665  cdleme22d  41666  cdleme22e  41667  cdleme22eALTN  41668  cdleme23b  41673  cdleme30a  41701  cdlemefrs29pre00  41718  cdlemefrs29bpre0  41719  cdlemefrs29cpre1  41721  cdleme32fva  41760  cdleme35b  41773  cdleme35d  41775  cdleme35e  41776  cdleme42a  41794  cdleme42ke  41808  cdlemeg46frv  41848  cdlemg2fv2  41923  cdlemg2m  41927  cdlemg10bALTN  41959  cdlemg12e  41970  cdlemg31d  42023  trlcoabs2N  42045  trlcolem  42049  trljco  42063  cdlemh2  42139  cdlemh  42140  cdlemi1  42141  cdlemk4  42157  cdlemk9  42162  cdlemk9bN  42163  cdlemkid2  42247  dia2dimlem1  42387  dia2dimlem2  42388  dia2dimlem3  42389  doca2N  42449  djajN  42460  cdlemn10  42529  dihvalcqat  42562  dih1  42609  dihglbcpreN  42623  dihmeetbclemN  42627  dihmeetlem7N  42633  dihjatc1  42634  djhlj  42724  djh01  42735  dihjatc  42740