Theorem hllatd 39364

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

Syntax hints:   → wi 4   ∈ wcel 2109  Latclat 18397  HLchlt 39350

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-dm 5651  df-iota 6467  df-fv 6522  df-ov 7393  df-atl 39298  df-cvlat 39322  df-hlat 39351

This theorem is referenced by:  hlrelat  39403  hlrelat2  39404  exatleN  39405  intnatN  39408  hlrelat3  39413  cvrval3  39414  cvrexchlem  39420  lnnat  39428  2atlt  39440  atexchcvrN  39441  atbtwn  39447  4noncolr3  39454  athgt  39457  3dim0  39458  3dimlem3a  39461  3dimlem4a  39464  3dim3  39470  1cvratex  39474  1cvrjat  39476  hlatexch4  39482  ps-2b  39483  3atlem1  39484  3atlem2  39485  3atlem4  39487  3atlem5  39488  3atlem6  39489  2llnmat  39525  2at0mat0  39526  2atm  39528  ps-2c  39529  llnmlplnN  39540  lplnle  39541  2atmat  39562  lplnexllnN  39565  2llnjaN  39567  lvoli3  39578  lvoli2  39582  lvolnle3at  39583  islvol2aN  39593  4atlem3  39597  4atlem3a  39598  4atlem3b  39599  4atlem4a  39600  4atlem4b  39601  4atlem4c  39602  4atlem4d  39603  4atlem9  39604  4atlem10a  39605  4atlem10  39607  4atlem11a  39608  4atlem11b  39609  4atlem11  39610  4atlem12a  39611  4atlem12b  39612  4atlem12  39613  4at  39614  4at2  39615  lplncvrlvol2  39616  lplncvrlvol  39617  2lplnja  39620  dalemkelat  39625  lneq2at  39779  lncmp  39784  2lnat  39785  cdlema1N  39792  cdlemblem  39794  cdlemb  39795  paddasslem2  39822  paddasslem5  39825  paddasslem8  39828  paddasslem12  39832  paddasslem13  39833  paddasslem15  39835  pmodlem1  39847  pmodlem2  39848  atmod1i1m  39859  llnmod1i2  39861  llnmod2i2  39864  llnexchb2lem  39869  llnexchb2  39870  dalawlem1  39872  dalawlem2  39873  dalawlem3  39874  dalawlem4  39875  dalawlem5  39876  dalawlem6  39877  dalawlem7  39878  dalawlem8  39879  dalawlem9  39880  dalawlem11  39882  dalawlem12  39883  dalawlem15  39886  pclfinclN  39951  poml4N  39954  osumcllem5N  39961  osumcllem7N  39963  pexmidlem2N  39972  pexmidlem4N  39974  pl42lem1N  39980  pl42lem2N  39981  pl42lem4N  39983  pl42N  39984  lhp2lt  40002  lhpexle2lem  40010  lhpexle3lem  40012  lhpj1  40023  lhpmcvr3  40026  lhpmcvr4N  40027  lhpmcvr5N  40028  lhpmcvr6N  40029  lhp2at0  40033  lhp2atnle  40034  lhpelim  40038  lhpmod2i2  40039  lhpmod6i1  40040  lhprelat3N  40041  lhple  40043  lhpat3  40047  4atexlemkl  40058  ltrnm  40132  ltrnj  40133  ltrnel  40140  ltrncnvel  40143  trljat1  40167  trljat2  40168  trlval3  40188  arglem1N  40191  cdlemc1  40192  cdlemc2  40193  cdlemc4  40195  cdlemc5  40196  cdlemc6  40197  cdlemd2  40200  cdlemd3  40201  cdlemd4  40202  cdlemd7  40205  cdleme0aa  40211  cdleme0b  40213  cdleme0c  40214  cdleme0e  40218  cdleme0fN  40219  cdlemeulpq  40221  cdleme01N  40222  cdleme0ex1N  40224  cdleme3g  40235  cdleme3h  40236  cdleme3  40238  cdleme4a  40240  cdleme5  40241  cdleme7aa  40243  cdleme7c  40246  cdleme7d  40247  cdleme7e  40248  cdleme7ga  40249  cdleme7  40250  cdleme8  40251  cdleme9  40254  cdleme10  40255  cdleme11c  40262  cdleme11e  40264  cdleme11fN  40265  cdleme11g  40266  cdleme11k  40269  cdleme11  40271  cdleme13  40273  cdleme15b  40276  cdleme15d  40278  cdleme15  40279  cdleme16b  40280  cdleme16e  40283  cdleme16f  40284  cdleme17b  40288  cdleme17c  40289  cdleme22gb  40295  cdlemednpq  40300  cdleme19b  40305  cdleme19c  40306  cdleme19e  40308  cdleme20aN  40310  cdleme20bN  40311  cdleme20c  40312  cdleme20d  40313  cdleme20e  40314  cdleme20j  40319  cdleme20k  40320  cdleme20l2  40322  cdleme20l  40323  cdleme20m  40324  cdleme21c  40328  cdleme21ct  40330  cdleme22aa  40340  cdleme22b  40342  cdleme22cN  40343  cdleme22d  40344  cdleme22e  40345  cdleme22eALTN  40346  cdleme22f  40347  cdleme22g  40349  cdleme23a  40350  cdleme23b  40351  cdleme23c  40352  cdleme27N  40370  cdleme28a  40371  cdleme28b  40372  cdleme29ex  40375  cdleme30a  40379  cdlemefr29exN  40403  cdleme32b  40443  cdleme32c  40444  cdleme32e  40446  cdleme35a  40449  cdleme35fnpq  40450  cdleme35b  40451  cdleme35c  40452  cdleme35d  40453  cdleme35f  40455  cdleme42c  40473  cdleme42e  40480  cdleme42h  40483  cdleme42i  40484  cdleme42mgN  40489  cdleme48bw  40503  cdlemeg46frv  40526  cdlemeg46vrg  40528  cdlemeg46rgv  40529  cdlemeg46req  40530  cdleme50eq  40542  cdlemf1  40562  trlord  40570  cdlemg2fv2  40601  cdlemg2m  40605  cdlemg7fvbwN  40608  cdlemg4c  40613  cdlemg4  40618  cdlemg6c  40621  cdlemg8b  40629  cdlemg10bALTN  40637  cdlemg10c  40640  cdlemg10  40642  cdlemg11b  40643  cdlemg12f  40649  cdlemg12g  40650  cdlemg12  40651  cdlemg13a  40652  cdlemg17a  40662  cdlemg17dALTN  40665  cdlemg17  40678  cdlemg18b  40680  cdlemg19a  40684  cdlemg19  40685  cdlemg27a  40693  cdlemg27b  40697  cdlemg31a  40698  cdlemg31b  40699  cdlemg33b0  40702  cdlemg33a  40707  cdlemg35  40714  trlcolem  40727  cdlemg42  40730  cdlemg44a  40732  cdlemg46  40736  trljco  40741  trljco2  40742  tendococl  40773  tendopltp  40781  cdlemh1  40816  cdlemh2  40817  cdlemi1  40819  cdlemi  40821  cdlemk3  40834  cdlemk4  40835  cdlemkvcl  40843  cdlemk10  40844  cdlemk7  40849  cdlemk11  40850  cdlemk12  40851  cdlemkole  40854  cdlemk14  40855  cdlemk15  40856  cdlemk1u  40860  cdlemk5u  40862  cdlemk7u  40871  cdlemk11u  40872  cdlemk12u  40873  cdlemk37  40915  cdlemk39  40917  cdlemkid1  40923  cdlemkid2  40925  cdlemk48  40951  cdlemk50  40953  cdlemk51  40954  cdlemk52  40955  cdlemk39u  40969  dia11N  41049  dia2dimlem1  41065  dia2dimlem2  41066  dia2dimlem3  41067  dia2dimlem10  41074  dia2dimlem12  41076  cdlemm10N  41119  dib11N  41161  diblss  41171  cdlemn2  41196  cdlemn10  41207  dihjustlem  41217  dihord1  41219  dihord2a  41220  dihord2b  41221  dihord2cN  41222  dihord11b  41223  dihord11c  41225  dihord2pre  41226  dihord2pre2  41227  dib2dim  41244  dih2dimb  41245  dihvalcq2  41248  dihopelvalcpre  41249  dihord6apre  41257  dihord5b  41260  dihord6b  41261  dihord5apre  41263  dih11  41266  dihwN  41290  dihmeetlem1N  41291  dihglblem5apreN  41292  dihglblem2N  41295  dihglblem3N  41296  dihmeetlem2N  41300  dihglbcpreN  41301  dihmeetbclemN  41305  dihmeetlem3N  41306  dihmeetlem4preN  41307  dihmeetlem6  41310  dihmeetlem7N  41311  dihjatc1  41312  dihjatc2N  41313  dihjatc3  41314  dihmeetlem9N  41316  dihmeetlem10N  41317  dihmeetlem11N  41318  dihmeetlem15N  41322  dihmeetlem16N  41323  dihmeetlem17N  41324  dihmeetlem19N  41326  dihmeetlem20N  41327  dihmeetALTN  41328  dihmeet2  41347  djhljjN  41403  djhj  41405  dihjatcclem1  41419  dihjatcclem2  41420  dihjatcclem4  41422  dihprrnlem1N  41425  dihprrnlem2  41426  dihjat6  41435  dihjat5N  41438  dvh4dimat  41439