Theorem hllatd 39382

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

Syntax hints:   → wi 4   ∈ wcel 2108  Latclat 18441  HLchlt 39368

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-dm 5664  df-iota 6484  df-fv 6539  df-ov 7408  df-atl 39316  df-cvlat 39340  df-hlat 39369

This theorem is referenced by:  hlrelat  39421  hlrelat2  39422  exatleN  39423  intnatN  39426  hlrelat3  39431  cvrval3  39432  cvrexchlem  39438  lnnat  39446  2atlt  39458  atexchcvrN  39459  atbtwn  39465  4noncolr3  39472  athgt  39475  3dim0  39476  3dimlem3a  39479  3dimlem4a  39482  3dim3  39488  1cvratex  39492  1cvrjat  39494  hlatexch4  39500  ps-2b  39501  3atlem1  39502  3atlem2  39503  3atlem4  39505  3atlem5  39506  3atlem6  39507  2llnmat  39543  2at0mat0  39544  2atm  39546  ps-2c  39547  llnmlplnN  39558  lplnle  39559  2atmat  39580  lplnexllnN  39583  2llnjaN  39585  lvoli3  39596  lvoli2  39600  lvolnle3at  39601  islvol2aN  39611  4atlem3  39615  4atlem3a  39616  4atlem3b  39617  4atlem4a  39618  4atlem4b  39619  4atlem4c  39620  4atlem4d  39621  4atlem9  39622  4atlem10a  39623  4atlem10  39625  4atlem11a  39626  4atlem11b  39627  4atlem11  39628  4atlem12a  39629  4atlem12b  39630  4atlem12  39631  4at  39632  4at2  39633  lplncvrlvol2  39634  lplncvrlvol  39635  2lplnja  39638  dalemkelat  39643  lneq2at  39797  lncmp  39802  2lnat  39803  cdlema1N  39810  cdlemblem  39812  cdlemb  39813  paddasslem2  39840  paddasslem5  39843  paddasslem8  39846  paddasslem12  39850  paddasslem13  39851  paddasslem15  39853  pmodlem1  39865  pmodlem2  39866  atmod1i1m  39877  llnmod1i2  39879  llnmod2i2  39882  llnexchb2lem  39887  llnexchb2  39888  dalawlem1  39890  dalawlem2  39891  dalawlem3  39892  dalawlem4  39893  dalawlem5  39894  dalawlem6  39895  dalawlem7  39896  dalawlem8  39897  dalawlem9  39898  dalawlem11  39900  dalawlem12  39901  dalawlem15  39904  pclfinclN  39969  poml4N  39972  osumcllem5N  39979  osumcllem7N  39981  pexmidlem2N  39990  pexmidlem4N  39992  pl42lem1N  39998  pl42lem2N  39999  pl42lem4N  40001  pl42N  40002  lhp2lt  40020  lhpexle2lem  40028  lhpexle3lem  40030  lhpj1  40041  lhpmcvr3  40044  lhpmcvr4N  40045  lhpmcvr5N  40046  lhpmcvr6N  40047  lhp2at0  40051  lhp2atnle  40052  lhpelim  40056  lhpmod2i2  40057  lhpmod6i1  40058  lhprelat3N  40059  lhple  40061  lhpat3  40065  4atexlemkl  40076  ltrnm  40150  ltrnj  40151  ltrnel  40158  ltrncnvel  40161  trljat1  40185  trljat2  40186  trlval3  40206  arglem1N  40209  cdlemc1  40210  cdlemc2  40211  cdlemc4  40213  cdlemc5  40214  cdlemc6  40215  cdlemd2  40218  cdlemd3  40219  cdlemd4  40220  cdlemd7  40223  cdleme0aa  40229  cdleme0b  40231  cdleme0c  40232  cdleme0e  40236  cdleme0fN  40237  cdlemeulpq  40239  cdleme01N  40240  cdleme0ex1N  40242  cdleme3g  40253  cdleme3h  40254  cdleme3  40256  cdleme4a  40258  cdleme5  40259  cdleme7aa  40261  cdleme7c  40264  cdleme7d  40265  cdleme7e  40266  cdleme7ga  40267  cdleme7  40268  cdleme8  40269  cdleme9  40272  cdleme10  40273  cdleme11c  40280  cdleme11e  40282  cdleme11fN  40283  cdleme11g  40284  cdleme11k  40287  cdleme11  40289  cdleme13  40291  cdleme15b  40294  cdleme15d  40296  cdleme15  40297  cdleme16b  40298  cdleme16e  40301  cdleme16f  40302  cdleme17b  40306  cdleme17c  40307  cdleme22gb  40313  cdlemednpq  40318  cdleme19b  40323  cdleme19c  40324  cdleme19e  40326  cdleme20aN  40328  cdleme20bN  40329  cdleme20c  40330  cdleme20d  40331  cdleme20e  40332  cdleme20j  40337  cdleme20k  40338  cdleme20l2  40340  cdleme20l  40341  cdleme20m  40342  cdleme21c  40346  cdleme21ct  40348  cdleme22aa  40358  cdleme22b  40360  cdleme22cN  40361  cdleme22d  40362  cdleme22e  40363  cdleme22eALTN  40364  cdleme22f  40365  cdleme22g  40367  cdleme23a  40368  cdleme23b  40369  cdleme23c  40370  cdleme27N  40388  cdleme28a  40389  cdleme28b  40390  cdleme29ex  40393  cdleme30a  40397  cdlemefr29exN  40421  cdleme32b  40461  cdleme32c  40462  cdleme32e  40464  cdleme35a  40467  cdleme35fnpq  40468  cdleme35b  40469  cdleme35c  40470  cdleme35d  40471  cdleme35f  40473  cdleme42c  40491  cdleme42e  40498  cdleme42h  40501  cdleme42i  40502  cdleme42mgN  40507  cdleme48bw  40521  cdlemeg46frv  40544  cdlemeg46vrg  40546  cdlemeg46rgv  40547  cdlemeg46req  40548  cdleme50eq  40560  cdlemf1  40580  trlord  40588  cdlemg2fv2  40619  cdlemg2m  40623  cdlemg7fvbwN  40626  cdlemg4c  40631  cdlemg4  40636  cdlemg6c  40639  cdlemg8b  40647  cdlemg10bALTN  40655  cdlemg10c  40658  cdlemg10  40660  cdlemg11b  40661  cdlemg12f  40667  cdlemg12g  40668  cdlemg12  40669  cdlemg13a  40670  cdlemg17a  40680  cdlemg17dALTN  40683  cdlemg17  40696  cdlemg18b  40698  cdlemg19a  40702  cdlemg19  40703  cdlemg27a  40711  cdlemg27b  40715  cdlemg31a  40716  cdlemg31b  40717  cdlemg33b0  40720  cdlemg33a  40725  cdlemg35  40732  trlcolem  40745  cdlemg42  40748  cdlemg44a  40750  cdlemg46  40754  trljco  40759  trljco2  40760  tendococl  40791  tendopltp  40799  cdlemh1  40834  cdlemh2  40835  cdlemi1  40837  cdlemi  40839  cdlemk3  40852  cdlemk4  40853  cdlemkvcl  40861  cdlemk10  40862  cdlemk7  40867  cdlemk11  40868  cdlemk12  40869  cdlemkole  40872  cdlemk14  40873  cdlemk15  40874  cdlemk1u  40878  cdlemk5u  40880  cdlemk7u  40889  cdlemk11u  40890  cdlemk12u  40891  cdlemk37  40933  cdlemk39  40935  cdlemkid1  40941  cdlemkid2  40943  cdlemk48  40969  cdlemk50  40971  cdlemk51  40972  cdlemk52  40973  cdlemk39u  40987  dia11N  41067  dia2dimlem1  41083  dia2dimlem2  41084  dia2dimlem3  41085  dia2dimlem10  41092  dia2dimlem12  41094  cdlemm10N  41137  dib11N  41179  diblss  41189  cdlemn2  41214  cdlemn10  41225  dihjustlem  41235  dihord1  41237  dihord2a  41238  dihord2b  41239  dihord2cN  41240  dihord11b  41241  dihord11c  41243  dihord2pre  41244  dihord2pre2  41245  dib2dim  41262  dih2dimb  41263  dihvalcq2  41266  dihopelvalcpre  41267  dihord6apre  41275  dihord5b  41278  dihord6b  41279  dihord5apre  41281  dih11  41284  dihwN  41308  dihmeetlem1N  41309  dihglblem5apreN  41310  dihglblem2N  41313  dihglblem3N  41314  dihmeetlem2N  41318  dihglbcpreN  41319  dihmeetbclemN  41323  dihmeetlem3N  41324  dihmeetlem4preN  41325  dihmeetlem6  41328  dihmeetlem7N  41329  dihjatc1  41330  dihjatc2N  41331  dihjatc3  41332  dihmeetlem9N  41334  dihmeetlem10N  41335  dihmeetlem11N  41336  dihmeetlem15N  41340  dihmeetlem16N  41341  dihmeetlem17N  41342  dihmeetlem19N  41344  dihmeetlem20N  41345  dihmeetALTN  41346  dihmeet2  41365  djhljjN  41421  djhj  41423  dihjatcclem1  41437  dihjatcclem2  41438  dihjatcclem4  41440  dihprrnlem1N  41443  dihprrnlem2  41444  dihjat6  41453  dihjat5N  41456  dvh4dimat  41457