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 2110  Latclat 18329  HLchlt 39368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-dm 5624  df-iota 6433  df-fv 6485  df-ov 7344  df-atl 39316  df-cvlat 39340  df-hlat 39369

This theorem is referenced by:  hlrelat  39420  hlrelat2  39421  exatleN  39422  intnatN  39425  hlrelat3  39430  cvrval3  39431  cvrexchlem  39437  lnnat  39445  2atlt  39457  atexchcvrN  39458  atbtwn  39464  4noncolr3  39471  athgt  39474  3dim0  39475  3dimlem3a  39478  3dimlem4a  39481  3dim3  39487  1cvratex  39491  1cvrjat  39493  hlatexch4  39499  ps-2b  39500  3atlem1  39501  3atlem2  39502  3atlem4  39504  3atlem5  39505  3atlem6  39506  2llnmat  39542  2at0mat0  39543  2atm  39545  ps-2c  39546  llnmlplnN  39557  lplnle  39558  2atmat  39579  lplnexllnN  39582  2llnjaN  39584  lvoli3  39595  lvoli2  39599  lvolnle3at  39600  islvol2aN  39610  4atlem3  39614  4atlem3a  39615  4atlem3b  39616  4atlem4a  39617  4atlem4b  39618  4atlem4c  39619  4atlem4d  39620  4atlem9  39621  4atlem10a  39622  4atlem10  39624  4atlem11a  39625  4atlem11b  39626  4atlem11  39627  4atlem12a  39628  4atlem12b  39629  4atlem12  39630  4at  39631  4at2  39632  lplncvrlvol2  39633  lplncvrlvol  39634  2lplnja  39637  dalemkelat  39642  lneq2at  39796  lncmp  39801  2lnat  39802  cdlema1N  39809  cdlemblem  39811  cdlemb  39812  paddasslem2  39839  paddasslem5  39842  paddasslem8  39845  paddasslem12  39849  paddasslem13  39850  paddasslem15  39852  pmodlem1  39864  pmodlem2  39865  atmod1i1m  39876  llnmod1i2  39878  llnmod2i2  39881  llnexchb2lem  39886  llnexchb2  39887  dalawlem1  39889  dalawlem2  39890  dalawlem3  39891  dalawlem4  39892  dalawlem5  39893  dalawlem6  39894  dalawlem7  39895  dalawlem8  39896  dalawlem9  39897  dalawlem11  39899  dalawlem12  39900  dalawlem15  39903  pclfinclN  39968  poml4N  39971  osumcllem5N  39978  osumcllem7N  39980  pexmidlem2N  39989  pexmidlem4N  39991  pl42lem1N  39997  pl42lem2N  39998  pl42lem4N  40000  pl42N  40001  lhp2lt  40019  lhpexle2lem  40027  lhpexle3lem  40029  lhpj1  40040  lhpmcvr3  40043  lhpmcvr4N  40044  lhpmcvr5N  40045  lhpmcvr6N  40046  lhp2at0  40050  lhp2atnle  40051  lhpelim  40055  lhpmod2i2  40056  lhpmod6i1  40057  lhprelat3N  40058  lhple  40060  lhpat3  40064  4atexlemkl  40075  ltrnm  40149  ltrnj  40150  ltrnel  40157  ltrncnvel  40160  trljat1  40184  trljat2  40185  trlval3  40205  arglem1N  40208  cdlemc1  40209  cdlemc2  40210  cdlemc4  40212  cdlemc5  40213  cdlemc6  40214  cdlemd2  40217  cdlemd3  40218  cdlemd4  40219  cdlemd7  40222  cdleme0aa  40228  cdleme0b  40230  cdleme0c  40231  cdleme0e  40235  cdleme0fN  40236  cdlemeulpq  40238  cdleme01N  40239  cdleme0ex1N  40241  cdleme3g  40252  cdleme3h  40253  cdleme3  40255  cdleme4a  40257  cdleme5  40258  cdleme7aa  40260  cdleme7c  40263  cdleme7d  40264  cdleme7e  40265  cdleme7ga  40266  cdleme7  40267  cdleme8  40268  cdleme9  40271  cdleme10  40272  cdleme11c  40279  cdleme11e  40281  cdleme11fN  40282  cdleme11g  40283  cdleme11k  40286  cdleme11  40288  cdleme13  40290  cdleme15b  40293  cdleme15d  40295  cdleme15  40296  cdleme16b  40297  cdleme16e  40300  cdleme16f  40301  cdleme17b  40305  cdleme17c  40306  cdleme22gb  40312  cdlemednpq  40317  cdleme19b  40322  cdleme19c  40323  cdleme19e  40325  cdleme20aN  40327  cdleme20bN  40328  cdleme20c  40329  cdleme20d  40330  cdleme20e  40331  cdleme20j  40336  cdleme20k  40337  cdleme20l2  40339  cdleme20l  40340  cdleme20m  40341  cdleme21c  40345  cdleme21ct  40347  cdleme22aa  40357  cdleme22b  40359  cdleme22cN  40360  cdleme22d  40361  cdleme22e  40362  cdleme22eALTN  40363  cdleme22f  40364  cdleme22g  40366  cdleme23a  40367  cdleme23b  40368  cdleme23c  40369  cdleme27N  40387  cdleme28a  40388  cdleme28b  40389  cdleme29ex  40392  cdleme30a  40396  cdlemefr29exN  40420  cdleme32b  40460  cdleme32c  40461  cdleme32e  40463  cdleme35a  40466  cdleme35fnpq  40467  cdleme35b  40468  cdleme35c  40469  cdleme35d  40470  cdleme35f  40472  cdleme42c  40490  cdleme42e  40497  cdleme42h  40500  cdleme42i  40501  cdleme42mgN  40506  cdleme48bw  40520  cdlemeg46frv  40543  cdlemeg46vrg  40545  cdlemeg46rgv  40546  cdlemeg46req  40547  cdleme50eq  40559  cdlemf1  40579  trlord  40587  cdlemg2fv2  40618  cdlemg2m  40622  cdlemg7fvbwN  40625  cdlemg4c  40630  cdlemg4  40635  cdlemg6c  40638  cdlemg8b  40646  cdlemg10bALTN  40654  cdlemg10c  40657  cdlemg10  40659  cdlemg11b  40660  cdlemg12f  40666  cdlemg12g  40667  cdlemg12  40668  cdlemg13a  40669  cdlemg17a  40679  cdlemg17dALTN  40682  cdlemg17  40695  cdlemg18b  40697  cdlemg19a  40701  cdlemg19  40702  cdlemg27a  40710  cdlemg27b  40714  cdlemg31a  40715  cdlemg31b  40716  cdlemg33b0  40719  cdlemg33a  40724  cdlemg35  40731  trlcolem  40744  cdlemg42  40747  cdlemg44a  40749  cdlemg46  40753  trljco  40758  trljco2  40759  tendococl  40790  tendopltp  40798  cdlemh1  40833  cdlemh2  40834  cdlemi1  40836  cdlemi  40838  cdlemk3  40851  cdlemk4  40852  cdlemkvcl  40860  cdlemk10  40861  cdlemk7  40866  cdlemk11  40867  cdlemk12  40868  cdlemkole  40871  cdlemk14  40872  cdlemk15  40873  cdlemk1u  40877  cdlemk5u  40879  cdlemk7u  40888  cdlemk11u  40889  cdlemk12u  40890  cdlemk37  40932  cdlemk39  40934  cdlemkid1  40940  cdlemkid2  40942  cdlemk48  40968  cdlemk50  40970  cdlemk51  40971  cdlemk52  40972  cdlemk39u  40986  dia11N  41066  dia2dimlem1  41082  dia2dimlem2  41083  dia2dimlem3  41084  dia2dimlem10  41091  dia2dimlem12  41093  cdlemm10N  41136  dib11N  41178  diblss  41188  cdlemn2  41213  cdlemn10  41224  dihjustlem  41234  dihord1  41236  dihord2a  41237  dihord2b  41238  dihord2cN  41239  dihord11b  41240  dihord11c  41242  dihord2pre  41243  dihord2pre2  41244  dib2dim  41261  dih2dimb  41262  dihvalcq2  41265  dihopelvalcpre  41266  dihord6apre  41274  dihord5b  41277  dihord6b  41278  dihord5apre  41280  dih11  41283  dihwN  41307  dihmeetlem1N  41308  dihglblem5apreN  41309  dihglblem2N  41312  dihglblem3N  41313  dihmeetlem2N  41317  dihglbcpreN  41318  dihmeetbclemN  41322  dihmeetlem3N  41323  dihmeetlem4preN  41324  dihmeetlem6  41327  dihmeetlem7N  41328  dihjatc1  41329  dihjatc2N  41330  dihjatc3  41331  dihmeetlem9N  41333  dihmeetlem10N  41334  dihmeetlem11N  41335  dihmeetlem15N  41339  dihmeetlem16N  41340  dihmeetlem17N  41341  dihmeetlem19N  41343  dihmeetlem20N  41344  dihmeetALTN  41345  dihmeet2  41364  djhljjN  41420  djhj  41422  dihjatcclem1  41436  dihjatcclem2  41437  dihjatcclem4  41439  dihprrnlem1N  41442  dihprrnlem2  41443  dihjat6  41452  dihjat5N  41455  dvh4dimat  41456