Theorem hlol 40512

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  OLcol 40325  OMLcoml 40326  HLchlt 40501

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6547  df-ov 7424  df-oml 40330  df-hlat 40502

This theorem is used by:  hlop  40513  cvrexch  40571  atle  40587  athgt  40607  2at0mat0  40676  dalem24  40848  pmapjat1  41004  atmod1i1m  41009  llnexchb2lem  41019  dalawlem2  41023  dalawlem6  41027  dalawlem7  41028  dalawlem11  41032  dalawlem12  41033  poldmj1N  41079  pmapj2N  41080  2polatN  41083  lhpmcvr3  41176  lhp2at0  41183  lhp2at0nle  41186  lhpelim  41188  lhpmod2i2  41189  lhpmod6i1  41190  lhprelat3N  41191  lhple  41193  4atex2-0aOLDN  41229  trljat1  41317  trljat2  41318  cdlemc1  41342  cdlemc6  41347  cdleme0cp  41365  cdleme0cq  41366  cdleme0e  41368  cdleme1  41378  cdleme2  41379  cdleme3c  41381  cdleme4  41389  cdleme5  41391  cdleme7c  41396  cdleme7e  41398  cdleme8  41401  cdleme9  41404  cdleme10  41405  cdleme15b  41426  cdlemednpq  41450  cdleme20c  41462  cdleme20d  41463  cdleme20j  41469  cdleme22cN  41493  cdleme22d  41494  cdleme22e  41495  cdleme22eALTN  41496  cdleme23b  41501  cdleme30a  41529  cdlemefrs29pre00  41546  cdlemefrs29bpre0  41547  cdlemefrs29cpre1  41549  cdleme32fva  41588  cdleme35b  41601  cdleme35d  41603  cdleme35e  41604  cdleme42a  41622  cdleme42ke  41636  cdlemeg46frv  41676  cdlemg2fv2  41751  cdlemg2m  41755  cdlemg10bALTN  41787  cdlemg12e  41798  cdlemg31d  41851  trlcoabs2N  41873  trlcolem  41877  trljco  41891  cdlemh2  41967  cdlemh  41968  cdlemi1  41969  cdlemk4  41985  cdlemk9  41990  cdlemk9bN  41991  cdlemkid2  42075  dia2dimlem1  42215  dia2dimlem2  42216  dia2dimlem3  42217  doca2N  42277  djajN  42288  cdlemn10  42357  dihvalcqat  42390  dih1  42437  dihglbcpreN  42451  dihmeetbclemN  42455  dihmeetlem7N  42461  dihjatc1  42462  djhlj  42552  djh01  42563  dihjatc  42568