Theorem hllatd 38222

Description: Deduction form of hllat 38221. 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 38221	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐾 ∈ Lat)

Syntax hints:   → wi 4   ∈ wcel 2106  Latclat 18380  HLchlt 38208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-dm 5685  df-iota 6492  df-fv 6548  df-ov 7408  df-atl 38156  df-cvlat 38180  df-hlat 38209

This theorem is referenced by:  hlrelat  38261  hlrelat2  38262  exatleN  38263  intnatN  38266  hlrelat3  38271  cvrval3  38272  cvrexchlem  38278  lnnat  38286  2atlt  38298  atexchcvrN  38299  atbtwn  38305  4noncolr3  38312  athgt  38315  3dim0  38316  3dimlem3a  38319  3dimlem4a  38322  3dim3  38328  1cvratex  38332  1cvrjat  38334  hlatexch4  38340  ps-2b  38341  3atlem1  38342  3atlem2  38343  3atlem4  38345  3atlem5  38346  3atlem6  38347  2llnmat  38383  2at0mat0  38384  2atm  38386  ps-2c  38387  llnmlplnN  38398  lplnle  38399  2atmat  38420  lplnexllnN  38423  2llnjaN  38425  lvoli3  38436  lvoli2  38440  lvolnle3at  38441  islvol2aN  38451  4atlem3  38455  4atlem3a  38456  4atlem3b  38457  4atlem4a  38458  4atlem4b  38459  4atlem4c  38460  4atlem4d  38461  4atlem9  38462  4atlem10a  38463  4atlem10  38465  4atlem11a  38466  4atlem11b  38467  4atlem11  38468  4atlem12a  38469  4atlem12b  38470  4atlem12  38471  4at  38472  4at2  38473  lplncvrlvol2  38474  lplncvrlvol  38475  2lplnja  38478  dalemkelat  38483  lneq2at  38637  lncmp  38642  2lnat  38643  cdlema1N  38650  cdlemblem  38652  cdlemb  38653  paddasslem2  38680  paddasslem5  38683  paddasslem8  38686  paddasslem12  38690  paddasslem13  38691  paddasslem15  38693  pmodlem1  38705  pmodlem2  38706  atmod1i1m  38717  llnmod1i2  38719  llnmod2i2  38722  llnexchb2lem  38727  llnexchb2  38728  dalawlem1  38730  dalawlem2  38731  dalawlem3  38732  dalawlem4  38733  dalawlem5  38734  dalawlem6  38735  dalawlem7  38736  dalawlem8  38737  dalawlem9  38738  dalawlem11  38740  dalawlem12  38741  dalawlem15  38744  pclfinclN  38809  poml4N  38812  osumcllem5N  38819  osumcllem7N  38821  pexmidlem2N  38830  pexmidlem4N  38832  pl42lem1N  38838  pl42lem2N  38839  pl42lem4N  38841  pl42N  38842  lhp2lt  38860  lhpexle2lem  38868  lhpexle3lem  38870  lhpj1  38881  lhpmcvr3  38884  lhpmcvr4N  38885  lhpmcvr5N  38886  lhpmcvr6N  38887  lhp2at0  38891  lhp2atnle  38892  lhpelim  38896  lhpmod2i2  38897  lhpmod6i1  38898  lhprelat3N  38899  lhple  38901  lhpat3  38905  4atexlemkl  38916  ltrnm  38990  ltrnj  38991  ltrnel  38998  ltrncnvel  39001  trljat1  39025  trljat2  39026  trlval3  39046  arglem1N  39049  cdlemc1  39050  cdlemc2  39051  cdlemc4  39053  cdlemc5  39054  cdlemc6  39055  cdlemd2  39058  cdlemd3  39059  cdlemd4  39060  cdlemd7  39063  cdleme0aa  39069  cdleme0b  39071  cdleme0c  39072  cdleme0e  39076  cdleme0fN  39077  cdlemeulpq  39079  cdleme01N  39080  cdleme0ex1N  39082  cdleme3g  39093  cdleme3h  39094  cdleme3  39096  cdleme4a  39098  cdleme5  39099  cdleme7aa  39101  cdleme7c  39104  cdleme7d  39105  cdleme7e  39106  cdleme7ga  39107  cdleme7  39108  cdleme8  39109  cdleme9  39112  cdleme10  39113  cdleme11c  39120  cdleme11e  39122  cdleme11fN  39123  cdleme11g  39124  cdleme11k  39127  cdleme11  39129  cdleme13  39131  cdleme15b  39134  cdleme15d  39136  cdleme15  39137  cdleme16b  39138  cdleme16e  39141  cdleme16f  39142  cdleme17b  39146  cdleme17c  39147  cdleme22gb  39153  cdlemednpq  39158  cdleme19b  39163  cdleme19c  39164  cdleme19e  39166  cdleme20aN  39168  cdleme20bN  39169  cdleme20c  39170  cdleme20d  39171  cdleme20e  39172  cdleme20j  39177  cdleme20k  39178  cdleme20l2  39180  cdleme20l  39181  cdleme20m  39182  cdleme21c  39186  cdleme21ct  39188  cdleme22aa  39198  cdleme22b  39200  cdleme22cN  39201  cdleme22d  39202  cdleme22e  39203  cdleme22eALTN  39204  cdleme22f  39205  cdleme22g  39207  cdleme23a  39208  cdleme23b  39209  cdleme23c  39210  cdleme27N  39228  cdleme28a  39229  cdleme28b  39230  cdleme29ex  39233  cdleme30a  39237  cdlemefr29exN  39261  cdleme32b  39301  cdleme32c  39302  cdleme32e  39304  cdleme35a  39307  cdleme35fnpq  39308  cdleme35b  39309  cdleme35c  39310  cdleme35d  39311  cdleme35f  39313  cdleme42c  39331  cdleme42e  39338  cdleme42h  39341  cdleme42i  39342  cdleme42mgN  39347  cdleme48bw  39361  cdlemeg46frv  39384  cdlemeg46vrg  39386  cdlemeg46rgv  39387  cdlemeg46req  39388  cdleme50eq  39400  cdlemf1  39420  trlord  39428  cdlemg2fv2  39459  cdlemg2m  39463  cdlemg7fvbwN  39466  cdlemg4c  39471  cdlemg4  39476  cdlemg6c  39479  cdlemg8b  39487  cdlemg10bALTN  39495  cdlemg10c  39498  cdlemg10  39500  cdlemg11b  39501  cdlemg12f  39507  cdlemg12g  39508  cdlemg12  39509  cdlemg13a  39510  cdlemg17a  39520  cdlemg17dALTN  39523  cdlemg17  39536  cdlemg18b  39538  cdlemg19a  39542  cdlemg19  39543  cdlemg27a  39551  cdlemg27b  39555  cdlemg31a  39556  cdlemg31b  39557  cdlemg33b0  39560  cdlemg33a  39565  cdlemg35  39572  trlcolem  39585  cdlemg42  39588  cdlemg44a  39590  cdlemg46  39594  trljco  39599  trljco2  39600  tendococl  39631  tendopltp  39639  cdlemh1  39674  cdlemh2  39675  cdlemi1  39677  cdlemi  39679  cdlemk3  39692  cdlemk4  39693  cdlemkvcl  39701  cdlemk10  39702  cdlemk7  39707  cdlemk11  39708  cdlemk12  39709  cdlemkole  39712  cdlemk14  39713  cdlemk15  39714  cdlemk1u  39718  cdlemk5u  39720  cdlemk7u  39729  cdlemk11u  39730  cdlemk12u  39731  cdlemk37  39773  cdlemk39  39775  cdlemkid1  39781  cdlemkid2  39783  cdlemk48  39809  cdlemk50  39811  cdlemk51  39812  cdlemk52  39813  cdlemk39u  39827  dia11N  39907  dia2dimlem1  39923  dia2dimlem2  39924  dia2dimlem3  39925  dia2dimlem10  39932  dia2dimlem12  39934  cdlemm10N  39977  dib11N  40019  diblss  40029  cdlemn2  40054  cdlemn10  40065  dihjustlem  40075  dihord1  40077  dihord2a  40078  dihord2b  40079  dihord2cN  40080  dihord11b  40081  dihord11c  40083  dihord2pre  40084  dihord2pre2  40085  dib2dim  40102  dih2dimb  40103  dihvalcq2  40106  dihopelvalcpre  40107  dihord6apre  40115  dihord5b  40118  dihord6b  40119  dihord5apre  40121  dih11  40124  dihwN  40148  dihmeetlem1N  40149  dihglblem5apreN  40150  dihglblem2N  40153  dihglblem3N  40154  dihmeetlem2N  40158  dihglbcpreN  40159  dihmeetbclemN  40163  dihmeetlem3N  40164  dihmeetlem4preN  40165  dihmeetlem6  40168  dihmeetlem7N  40169  dihjatc1  40170  dihjatc2N  40171  dihjatc3  40172  dihmeetlem9N  40174  dihmeetlem10N  40175  dihmeetlem11N  40176  dihmeetlem15N  40180  dihmeetlem16N  40181  dihmeetlem17N  40182  dihmeetlem19N  40184  dihmeetlem20N  40185  dihmeetALTN  40186  dihmeet2  40205  djhljjN  40261  djhj  40263  dihjatcclem1  40277  dihjatcclem2  40278  dihjatcclem4  40280  dihprrnlem1N  40283  dihprrnlem2  40284  dihjat6  40293  dihjat5N  40296  dvh4dimat  40297