Theorem hllatd 39330

Description: Deduction form of hllat 39329. A Hilbert lattice is a lattice. (Contributed by BJ, 14-Aug-2022.)

Hypothesis

Ref	Expression
hllatd.1	⊢ (𝜑 → 𝐾 ∈ HL)

Assertion

Ref	Expression
hllatd	⊢ (𝜑 → 𝐾 ∈ Lat)

Proof of Theorem hllatd

Step	Hyp	Ref	Expression
1		hllatd.1	. 2 ⊢ (𝜑 → 𝐾 ∈ HL)
2		hllat 39329	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐾 ∈ Lat)

Syntax hints:   → wi 4   ∈ wcel 2109  Latclat 18366  HLchlt 39316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-dm 5641  df-iota 6452  df-fv 6507  df-ov 7372  df-atl 39264  df-cvlat 39288  df-hlat 39317

This theorem is referenced by:  hlrelat  39369  hlrelat2  39370  exatleN  39371  intnatN  39374  hlrelat3  39379  cvrval3  39380  cvrexchlem  39386  lnnat  39394  2atlt  39406  atexchcvrN  39407  atbtwn  39413  4noncolr3  39420  athgt  39423  3dim0  39424  3dimlem3a  39427  3dimlem4a  39430  3dim3  39436  1cvratex  39440  1cvrjat  39442  hlatexch4  39448  ps-2b  39449  3atlem1  39450  3atlem2  39451  3atlem4  39453  3atlem5  39454  3atlem6  39455  2llnmat  39491  2at0mat0  39492  2atm  39494  ps-2c  39495  llnmlplnN  39506  lplnle  39507  2atmat  39528  lplnexllnN  39531  2llnjaN  39533  lvoli3  39544  lvoli2  39548  lvolnle3at  39549  islvol2aN  39559  4atlem3  39563  4atlem3a  39564  4atlem3b  39565  4atlem4a  39566  4atlem4b  39567  4atlem4c  39568  4atlem4d  39569  4atlem9  39570  4atlem10a  39571  4atlem10  39573  4atlem11a  39574  4atlem11b  39575  4atlem11  39576  4atlem12a  39577  4atlem12b  39578  4atlem12  39579  4at  39580  4at2  39581  lplncvrlvol2  39582  lplncvrlvol  39583  2lplnja  39586  dalemkelat  39591  lneq2at  39745  lncmp  39750  2lnat  39751  cdlema1N  39758  cdlemblem  39760  cdlemb  39761  paddasslem2  39788  paddasslem5  39791  paddasslem8  39794  paddasslem12  39798  paddasslem13  39799  paddasslem15  39801  pmodlem1  39813  pmodlem2  39814  atmod1i1m  39825  llnmod1i2  39827  llnmod2i2  39830  llnexchb2lem  39835  llnexchb2  39836  dalawlem1  39838  dalawlem2  39839  dalawlem3  39840  dalawlem4  39841  dalawlem5  39842  dalawlem6  39843  dalawlem7  39844  dalawlem8  39845  dalawlem9  39846  dalawlem11  39848  dalawlem12  39849  dalawlem15  39852  pclfinclN  39917  poml4N  39920  osumcllem5N  39927  osumcllem7N  39929  pexmidlem2N  39938  pexmidlem4N  39940  pl42lem1N  39946  pl42lem2N  39947  pl42lem4N  39949  pl42N  39950  lhp2lt  39968  lhpexle2lem  39976  lhpexle3lem  39978  lhpj1  39989  lhpmcvr3  39992  lhpmcvr4N  39993  lhpmcvr5N  39994  lhpmcvr6N  39995  lhp2at0  39999  lhp2atnle  40000  lhpelim  40004  lhpmod2i2  40005  lhpmod6i1  40006  lhprelat3N  40007  lhple  40009  lhpat3  40013  4atexlemkl  40024  ltrnm  40098  ltrnj  40099  ltrnel  40106  ltrncnvel  40109  trljat1  40133  trljat2  40134  trlval3  40154  arglem1N  40157  cdlemc1  40158  cdlemc2  40159  cdlemc4  40161  cdlemc5  40162  cdlemc6  40163  cdlemd2  40166  cdlemd3  40167  cdlemd4  40168  cdlemd7  40171  cdleme0aa  40177  cdleme0b  40179  cdleme0c  40180  cdleme0e  40184  cdleme0fN  40185  cdlemeulpq  40187  cdleme01N  40188  cdleme0ex1N  40190  cdleme3g  40201  cdleme3h  40202  cdleme3  40204  cdleme4a  40206  cdleme5  40207  cdleme7aa  40209  cdleme7c  40212  cdleme7d  40213  cdleme7e  40214  cdleme7ga  40215  cdleme7  40216  cdleme8  40217  cdleme9  40220  cdleme10  40221  cdleme11c  40228  cdleme11e  40230  cdleme11fN  40231  cdleme11g  40232  cdleme11k  40235  cdleme11  40237  cdleme13  40239  cdleme15b  40242  cdleme15d  40244  cdleme15  40245  cdleme16b  40246  cdleme16e  40249  cdleme16f  40250  cdleme17b  40254  cdleme17c  40255  cdleme22gb  40261  cdlemednpq  40266  cdleme19b  40271  cdleme19c  40272  cdleme19e  40274  cdleme20aN  40276  cdleme20bN  40277  cdleme20c  40278  cdleme20d  40279  cdleme20e  40280  cdleme20j  40285  cdleme20k  40286  cdleme20l2  40288  cdleme20l  40289  cdleme20m  40290  cdleme21c  40294  cdleme21ct  40296  cdleme22aa  40306  cdleme22b  40308  cdleme22cN  40309  cdleme22d  40310  cdleme22e  40311  cdleme22eALTN  40312  cdleme22f  40313  cdleme22g  40315  cdleme23a  40316  cdleme23b  40317  cdleme23c  40318  cdleme27N  40336  cdleme28a  40337  cdleme28b  40338  cdleme29ex  40341  cdleme30a  40345  cdlemefr29exN  40369  cdleme32b  40409  cdleme32c  40410  cdleme32e  40412  cdleme35a  40415  cdleme35fnpq  40416  cdleme35b  40417  cdleme35c  40418  cdleme35d  40419  cdleme35f  40421  cdleme42c  40439  cdleme42e  40446  cdleme42h  40449  cdleme42i  40450  cdleme42mgN  40455  cdleme48bw  40469  cdlemeg46frv  40492  cdlemeg46vrg  40494  cdlemeg46rgv  40495  cdlemeg46req  40496  cdleme50eq  40508  cdlemf1  40528  trlord  40536  cdlemg2fv2  40567  cdlemg2m  40571  cdlemg7fvbwN  40574  cdlemg4c  40579  cdlemg4  40584  cdlemg6c  40587  cdlemg8b  40595  cdlemg10bALTN  40603  cdlemg10c  40606  cdlemg10  40608  cdlemg11b  40609  cdlemg12f  40615  cdlemg12g  40616  cdlemg12  40617  cdlemg13a  40618  cdlemg17a  40628  cdlemg17dALTN  40631  cdlemg17  40644  cdlemg18b  40646  cdlemg19a  40650  cdlemg19  40651  cdlemg27a  40659  cdlemg27b  40663  cdlemg31a  40664  cdlemg31b  40665  cdlemg33b0  40668  cdlemg33a  40673  cdlemg35  40680  trlcolem  40693  cdlemg42  40696  cdlemg44a  40698  cdlemg46  40702  trljco  40707  trljco2  40708  tendococl  40739  tendopltp  40747  cdlemh1  40782  cdlemh2  40783  cdlemi1  40785  cdlemi  40787  cdlemk3  40800  cdlemk4  40801  cdlemkvcl  40809  cdlemk10  40810  cdlemk7  40815  cdlemk11  40816  cdlemk12  40817  cdlemkole  40820  cdlemk14  40821  cdlemk15  40822  cdlemk1u  40826  cdlemk5u  40828  cdlemk7u  40837  cdlemk11u  40838  cdlemk12u  40839  cdlemk37  40881  cdlemk39  40883  cdlemkid1  40889  cdlemkid2  40891  cdlemk48  40917  cdlemk50  40919  cdlemk51  40920  cdlemk52  40921  cdlemk39u  40935  dia11N  41015  dia2dimlem1  41031  dia2dimlem2  41032  dia2dimlem3  41033  dia2dimlem10  41040  dia2dimlem12  41042  cdlemm10N  41085  dib11N  41127  diblss  41137  cdlemn2  41162  cdlemn10  41173  dihjustlem  41183  dihord1  41185  dihord2a  41186  dihord2b  41187  dihord2cN  41188  dihord11b  41189  dihord11c  41191  dihord2pre  41192  dihord2pre2  41193  dib2dim  41210  dih2dimb  41211  dihvalcq2  41214  dihopelvalcpre  41215  dihord6apre  41223  dihord5b  41226  dihord6b  41227  dihord5apre  41229  dih11  41232  dihwN  41256  dihmeetlem1N  41257  dihglblem5apreN  41258  dihglblem2N  41261  dihglblem3N  41262  dihmeetlem2N  41266  dihglbcpreN  41267  dihmeetbclemN  41271  dihmeetlem3N  41272  dihmeetlem4preN  41273  dihmeetlem6  41276  dihmeetlem7N  41277  dihjatc1  41278  dihjatc2N  41279  dihjatc3  41280  dihmeetlem9N  41282  dihmeetlem10N  41283  dihmeetlem11N  41284  dihmeetlem15N  41288  dihmeetlem16N  41289  dihmeetlem17N  41290  dihmeetlem19N  41292  dihmeetlem20N  41293  dihmeetALTN  41294  dihmeet2  41313  djhljjN  41369  djhj  41371  dihjatcclem1  41385  dihjatcclem2  41386  dihjatcclem4  41388  dihprrnlem1N  41391  dihprrnlem2  41392  dihjat6  41401  dihjat5N  41404  dvh4dimat  41405