Theorem hllatd 40158

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

Syntax hints:   → wi 4   ∈ wcel 2143  Latclat 18482  HLchlt 40144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-dm 5671  df-iota 6492  df-fv 6544  df-ov 7413  df-atl 40092  df-cvlat 40116  df-hlat 40145

This theorem is referenced by:  hlrelat  40196  hlrelat2  40197  exatleN  40198  intnatN  40201  hlrelat3  40206  cvrval3  40207  cvrexchlem  40213  lnnat  40221  2atlt  40233  atexchcvrN  40234  atbtwn  40240  4noncolr3  40247  athgt  40250  3dim0  40251  3dimlem3a  40254  3dimlem4a  40257  3dim3  40263  1cvratex  40267  1cvrjat  40269  hlatexch4  40275  ps-2b  40276  3atlem1  40277  3atlem2  40278  3atlem4  40280  3atlem5  40281  3atlem6  40282  2llnmat  40318  2at0mat0  40319  2atm  40321  ps-2c  40322  llnmlplnN  40333  lplnle  40334  2atmat  40355  lplnexllnN  40358  2llnjaN  40360  lvoli3  40371  lvoli2  40375  lvolnle3at  40376  islvol2aN  40386  4atlem3  40390  4atlem3a  40391  4atlem3b  40392  4atlem4a  40393  4atlem4b  40394  4atlem4c  40395  4atlem4d  40396  4atlem9  40397  4atlem10a  40398  4atlem10  40400  4atlem11a  40401  4atlem11b  40402  4atlem11  40403  4atlem12a  40404  4atlem12b  40405  4atlem12  40406  4at  40407  4at2  40408  lplncvrlvol2  40409  lplncvrlvol  40410  2lplnja  40413  dalemkelat  40418  lneq2at  40572  lncmp  40577  2lnat  40578  cdlema1N  40585  cdlemblem  40587  cdlemb  40588  paddasslem2  40615  paddasslem5  40618  paddasslem8  40621  paddasslem12  40625  paddasslem13  40626  paddasslem15  40628  pmodlem1  40640  pmodlem2  40641  atmod1i1m  40652  llnmod1i2  40654  llnmod2i2  40657  llnexchb2lem  40662  llnexchb2  40663  dalawlem1  40665  dalawlem2  40666  dalawlem3  40667  dalawlem4  40668  dalawlem5  40669  dalawlem6  40670  dalawlem7  40671  dalawlem8  40672  dalawlem9  40673  dalawlem11  40675  dalawlem12  40676  dalawlem15  40679  pclfinclN  40744  poml4N  40747  osumcllem5N  40754  osumcllem7N  40756  pexmidlem2N  40765  pexmidlem4N  40767  pl42lem1N  40773  pl42lem2N  40774  pl42lem4N  40776  pl42N  40777  lhp2lt  40795  lhpexle2lem  40803  lhpexle3lem  40805  lhpj1  40816  lhpmcvr3  40819  lhpmcvr4N  40820  lhpmcvr5N  40821  lhpmcvr6N  40822  lhp2at0  40826  lhp2atnle  40827  lhpelim  40831  lhpmod2i2  40832  lhpmod6i1  40833  lhprelat3N  40834  lhple  40836  lhpat3  40840  4atexlemkl  40851  ltrnm  40925  ltrnj  40926  ltrnel  40933  ltrncnvel  40936  trljat1  40960  trljat2  40961  trlval3  40981  arglem1N  40984  cdlemc1  40985  cdlemc2  40986  cdlemc4  40988  cdlemc5  40989  cdlemc6  40990  cdlemd2  40993  cdlemd3  40994  cdlemd4  40995  cdlemd7  40998  cdleme0aa  41004  cdleme0b  41006  cdleme0c  41007  cdleme0e  41011  cdleme0fN  41012  cdlemeulpq  41014  cdleme01N  41015  cdleme0ex1N  41017  cdleme3g  41028  cdleme3h  41029  cdleme3  41031  cdleme4a  41033  cdleme5  41034  cdleme7aa  41036  cdleme7c  41039  cdleme7d  41040  cdleme7e  41041  cdleme7ga  41042  cdleme7  41043  cdleme8  41044  cdleme9  41047  cdleme10  41048  cdleme11c  41055  cdleme11e  41057  cdleme11fN  41058  cdleme11g  41059  cdleme11k  41062  cdleme11  41064  cdleme13  41066  cdleme15b  41069  cdleme15d  41071  cdleme15  41072  cdleme16b  41073  cdleme16e  41076  cdleme16f  41077  cdleme17b  41081  cdleme17c  41082  cdleme22gb  41088  cdlemednpq  41093  cdleme19b  41098  cdleme19c  41099  cdleme19e  41101  cdleme20aN  41103  cdleme20bN  41104  cdleme20c  41105  cdleme20d  41106  cdleme20e  41107  cdleme20j  41112  cdleme20k  41113  cdleme20l2  41115  cdleme20l  41116  cdleme20m  41117  cdleme21c  41121  cdleme21ct  41123  cdleme22aa  41133  cdleme22b  41135  cdleme22cN  41136  cdleme22d  41137  cdleme22e  41138  cdleme22eALTN  41139  cdleme22f  41140  cdleme22g  41142  cdleme23a  41143  cdleme23b  41144  cdleme23c  41145  cdleme27N  41163  cdleme28a  41164  cdleme28b  41165  cdleme29ex  41168  cdleme30a  41172  cdlemefr29exN  41196  cdleme32b  41236  cdleme32c  41237  cdleme32e  41239  cdleme35a  41242  cdleme35fnpq  41243  cdleme35b  41244  cdleme35c  41245  cdleme35d  41246  cdleme35f  41248  cdleme42c  41266  cdleme42e  41273  cdleme42h  41276  cdleme42i  41277  cdleme42mgN  41282  cdleme48bw  41296  cdlemeg46frv  41319  cdlemeg46vrg  41321  cdlemeg46rgv  41322  cdlemeg46req  41323  cdleme50eq  41335  cdlemf1  41355  trlord  41363  cdlemg2fv2  41394  cdlemg2m  41398  cdlemg7fvbwN  41401  cdlemg4c  41406  cdlemg4  41411  cdlemg6c  41414  cdlemg8b  41422  cdlemg10bALTN  41430  cdlemg10c  41433  cdlemg10  41435  cdlemg11b  41436  cdlemg12f  41442  cdlemg12g  41443  cdlemg12  41444  cdlemg13a  41445  cdlemg17a  41455  cdlemg17dALTN  41458  cdlemg17  41471  cdlemg18b  41473  cdlemg19a  41477  cdlemg19  41478  cdlemg27a  41486  cdlemg27b  41490  cdlemg31a  41491  cdlemg31b  41492  cdlemg33b0  41495  cdlemg33a  41500  cdlemg35  41507  trlcolem  41520  cdlemg42  41523  cdlemg44a  41525  cdlemg46  41529  trljco  41534  trljco2  41535  tendococl  41566  tendopltp  41574  cdlemh1  41609  cdlemh2  41610  cdlemi1  41612  cdlemi  41614  cdlemk3  41627  cdlemk4  41628  cdlemkvcl  41636  cdlemk10  41637  cdlemk7  41642  cdlemk11  41643  cdlemk12  41644  cdlemkole  41647  cdlemk14  41648  cdlemk15  41649  cdlemk1u  41653  cdlemk5u  41655  cdlemk7u  41664  cdlemk11u  41665  cdlemk12u  41666  cdlemk37  41708  cdlemk39  41710  cdlemkid1  41716  cdlemkid2  41718  cdlemk48  41744  cdlemk50  41746  cdlemk51  41747  cdlemk52  41748  cdlemk39u  41762  dia11N  41842  dia2dimlem1  41858  dia2dimlem2  41859  dia2dimlem3  41860  dia2dimlem10  41867  dia2dimlem12  41869  cdlemm10N  41912  dib11N  41954  diblss  41964  cdlemn2  41989  cdlemn10  42000  dihjustlem  42010  dihord1  42012  dihord2a  42013  dihord2b  42014  dihord2cN  42015  dihord11b  42016  dihord11c  42018  dihord2pre  42019  dihord2pre2  42020  dib2dim  42037  dih2dimb  42038  dihvalcq2  42041  dihopelvalcpre  42042  dihord6apre  42050  dihord5b  42053  dihord6b  42054  dihord5apre  42056  dih11  42059  dihwN  42083  dihmeetlem1N  42084  dihglblem5apreN  42085  dihglblem2N  42088  dihglblem3N  42089  dihmeetlem2N  42093  dihglbcpreN  42094  dihmeetbclemN  42098  dihmeetlem3N  42099  dihmeetlem4preN  42100  dihmeetlem6  42103  dihmeetlem7N  42104  dihjatc1  42105  dihjatc2N  42106  dihjatc3  42107  dihmeetlem9N  42109  dihmeetlem10N  42110  dihmeetlem11N  42111  dihmeetlem15N  42115  dihmeetlem16N  42116  dihmeetlem17N  42117  dihmeetlem19N  42119  dihmeetlem20N  42120  dihmeetALTN  42121  dihmeet2  42140  djhljjN  42196  djhj  42198  dihjatcclem1  42212  dihjatcclem2  42213  dihjatcclem4  42215  dihprrnlem1N  42218  dihprrnlem2  42219  dihjat6  42228  dihjat5N  42231  dvh4dimat  42232