Theorem hllatd 39320

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

Syntax hints:   → wi 4   ∈ wcel 2108  Latclat 18501  HLchlt 39306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-dm 5710  df-iota 6525  df-fv 6581  df-ov 7451  df-atl 39254  df-cvlat 39278  df-hlat 39307

This theorem is referenced by:  hlrelat  39359  hlrelat2  39360  exatleN  39361  intnatN  39364  hlrelat3  39369  cvrval3  39370  cvrexchlem  39376  lnnat  39384  2atlt  39396  atexchcvrN  39397  atbtwn  39403  4noncolr3  39410  athgt  39413  3dim0  39414  3dimlem3a  39417  3dimlem4a  39420  3dim3  39426  1cvratex  39430  1cvrjat  39432  hlatexch4  39438  ps-2b  39439  3atlem1  39440  3atlem2  39441  3atlem4  39443  3atlem5  39444  3atlem6  39445  2llnmat  39481  2at0mat0  39482  2atm  39484  ps-2c  39485  llnmlplnN  39496  lplnle  39497  2atmat  39518  lplnexllnN  39521  2llnjaN  39523  lvoli3  39534  lvoli2  39538  lvolnle3at  39539  islvol2aN  39549  4atlem3  39553  4atlem3a  39554  4atlem3b  39555  4atlem4a  39556  4atlem4b  39557  4atlem4c  39558  4atlem4d  39559  4atlem9  39560  4atlem10a  39561  4atlem10  39563  4atlem11a  39564  4atlem11b  39565  4atlem11  39566  4atlem12a  39567  4atlem12b  39568  4atlem12  39569  4at  39570  4at2  39571  lplncvrlvol2  39572  lplncvrlvol  39573  2lplnja  39576  dalemkelat  39581  lneq2at  39735  lncmp  39740  2lnat  39741  cdlema1N  39748  cdlemblem  39750  cdlemb  39751  paddasslem2  39778  paddasslem5  39781  paddasslem8  39784  paddasslem12  39788  paddasslem13  39789  paddasslem15  39791  pmodlem1  39803  pmodlem2  39804  atmod1i1m  39815  llnmod1i2  39817  llnmod2i2  39820  llnexchb2lem  39825  llnexchb2  39826  dalawlem1  39828  dalawlem2  39829  dalawlem3  39830  dalawlem4  39831  dalawlem5  39832  dalawlem6  39833  dalawlem7  39834  dalawlem8  39835  dalawlem9  39836  dalawlem11  39838  dalawlem12  39839  dalawlem15  39842  pclfinclN  39907  poml4N  39910  osumcllem5N  39917  osumcllem7N  39919  pexmidlem2N  39928  pexmidlem4N  39930  pl42lem1N  39936  pl42lem2N  39937  pl42lem4N  39939  pl42N  39940  lhp2lt  39958  lhpexle2lem  39966  lhpexle3lem  39968  lhpj1  39979  lhpmcvr3  39982  lhpmcvr4N  39983  lhpmcvr5N  39984  lhpmcvr6N  39985  lhp2at0  39989  lhp2atnle  39990  lhpelim  39994  lhpmod2i2  39995  lhpmod6i1  39996  lhprelat3N  39997  lhple  39999  lhpat3  40003  4atexlemkl  40014  ltrnm  40088  ltrnj  40089  ltrnel  40096  ltrncnvel  40099  trljat1  40123  trljat2  40124  trlval3  40144  arglem1N  40147  cdlemc1  40148  cdlemc2  40149  cdlemc4  40151  cdlemc5  40152  cdlemc6  40153  cdlemd2  40156  cdlemd3  40157  cdlemd4  40158  cdlemd7  40161  cdleme0aa  40167  cdleme0b  40169  cdleme0c  40170  cdleme0e  40174  cdleme0fN  40175  cdlemeulpq  40177  cdleme01N  40178  cdleme0ex1N  40180  cdleme3g  40191  cdleme3h  40192  cdleme3  40194  cdleme4a  40196  cdleme5  40197  cdleme7aa  40199  cdleme7c  40202  cdleme7d  40203  cdleme7e  40204  cdleme7ga  40205  cdleme7  40206  cdleme8  40207  cdleme9  40210  cdleme10  40211  cdleme11c  40218  cdleme11e  40220  cdleme11fN  40221  cdleme11g  40222  cdleme11k  40225  cdleme11  40227  cdleme13  40229  cdleme15b  40232  cdleme15d  40234  cdleme15  40235  cdleme16b  40236  cdleme16e  40239  cdleme16f  40240  cdleme17b  40244  cdleme17c  40245  cdleme22gb  40251  cdlemednpq  40256  cdleme19b  40261  cdleme19c  40262  cdleme19e  40264  cdleme20aN  40266  cdleme20bN  40267  cdleme20c  40268  cdleme20d  40269  cdleme20e  40270  cdleme20j  40275  cdleme20k  40276  cdleme20l2  40278  cdleme20l  40279  cdleme20m  40280  cdleme21c  40284  cdleme21ct  40286  cdleme22aa  40296  cdleme22b  40298  cdleme22cN  40299  cdleme22d  40300  cdleme22e  40301  cdleme22eALTN  40302  cdleme22f  40303  cdleme22g  40305  cdleme23a  40306  cdleme23b  40307  cdleme23c  40308  cdleme27N  40326  cdleme28a  40327  cdleme28b  40328  cdleme29ex  40331  cdleme30a  40335  cdlemefr29exN  40359  cdleme32b  40399  cdleme32c  40400  cdleme32e  40402  cdleme35a  40405  cdleme35fnpq  40406  cdleme35b  40407  cdleme35c  40408  cdleme35d  40409  cdleme35f  40411  cdleme42c  40429  cdleme42e  40436  cdleme42h  40439  cdleme42i  40440  cdleme42mgN  40445  cdleme48bw  40459  cdlemeg46frv  40482  cdlemeg46vrg  40484  cdlemeg46rgv  40485  cdlemeg46req  40486  cdleme50eq  40498  cdlemf1  40518  trlord  40526  cdlemg2fv2  40557  cdlemg2m  40561  cdlemg7fvbwN  40564  cdlemg4c  40569  cdlemg4  40574  cdlemg6c  40577  cdlemg8b  40585  cdlemg10bALTN  40593  cdlemg10c  40596  cdlemg10  40598  cdlemg11b  40599  cdlemg12f  40605  cdlemg12g  40606  cdlemg12  40607  cdlemg13a  40608  cdlemg17a  40618  cdlemg17dALTN  40621  cdlemg17  40634  cdlemg18b  40636  cdlemg19a  40640  cdlemg19  40641  cdlemg27a  40649  cdlemg27b  40653  cdlemg31a  40654  cdlemg31b  40655  cdlemg33b0  40658  cdlemg33a  40663  cdlemg35  40670  trlcolem  40683  cdlemg42  40686  cdlemg44a  40688  cdlemg46  40692  trljco  40697  trljco2  40698  tendococl  40729  tendopltp  40737  cdlemh1  40772  cdlemh2  40773  cdlemi1  40775  cdlemi  40777  cdlemk3  40790  cdlemk4  40791  cdlemkvcl  40799  cdlemk10  40800  cdlemk7  40805  cdlemk11  40806  cdlemk12  40807  cdlemkole  40810  cdlemk14  40811  cdlemk15  40812  cdlemk1u  40816  cdlemk5u  40818  cdlemk7u  40827  cdlemk11u  40828  cdlemk12u  40829  cdlemk37  40871  cdlemk39  40873  cdlemkid1  40879  cdlemkid2  40881  cdlemk48  40907  cdlemk50  40909  cdlemk51  40910  cdlemk52  40911  cdlemk39u  40925  dia11N  41005  dia2dimlem1  41021  dia2dimlem2  41022  dia2dimlem3  41023  dia2dimlem10  41030  dia2dimlem12  41032  cdlemm10N  41075  dib11N  41117  diblss  41127  cdlemn2  41152  cdlemn10  41163  dihjustlem  41173  dihord1  41175  dihord2a  41176  dihord2b  41177  dihord2cN  41178  dihord11b  41179  dihord11c  41181  dihord2pre  41182  dihord2pre2  41183  dib2dim  41200  dih2dimb  41201  dihvalcq2  41204  dihopelvalcpre  41205  dihord6apre  41213  dihord5b  41216  dihord6b  41217  dihord5apre  41219  dih11  41222  dihwN  41246  dihmeetlem1N  41247  dihglblem5apreN  41248  dihglblem2N  41251  dihglblem3N  41252  dihmeetlem2N  41256  dihglbcpreN  41257  dihmeetbclemN  41261  dihmeetlem3N  41262  dihmeetlem4preN  41263  dihmeetlem6  41266  dihmeetlem7N  41267  dihjatc1  41268  dihjatc2N  41269  dihjatc3  41270  dihmeetlem9N  41272  dihmeetlem10N  41273  dihmeetlem11N  41274  dihmeetlem15N  41278  dihmeetlem16N  41279  dihmeetlem17N  41280  dihmeetlem19N  41282  dihmeetlem20N  41283  dihmeetALTN  41284  dihmeet2  41303  djhljjN  41359  djhj  41361  dihjatcclem1  41375  dihjatcclem2  41376  dihjatcclem4  41378  dihprrnlem1N  41381  dihprrnlem2  41382  dihjat6  41391  dihjat5N  41394  dvh4dimat  41395