Theorem hllatd 37115

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

Syntax hints:   → wi 4   ∈ wcel 2110  Latclat 17937  HLchlt 37101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-dm 5561  df-iota 6338  df-fv 6388  df-ov 7216  df-atl 37049  df-cvlat 37073  df-hlat 37102

This theorem is referenced by:  hlrelat  37153  hlrelat2  37154  exatleN  37155  intnatN  37158  hlrelat3  37163  cvrval3  37164  cvrexchlem  37170  lnnat  37178  2atlt  37190  atexchcvrN  37191  atbtwn  37197  4noncolr3  37204  athgt  37207  3dim0  37208  3dimlem3a  37211  3dimlem4a  37214  3dim3  37220  1cvratex  37224  1cvrjat  37226  hlatexch4  37232  ps-2b  37233  3atlem1  37234  3atlem2  37235  3atlem4  37237  3atlem5  37238  3atlem6  37239  2llnmat  37275  2at0mat0  37276  2atm  37278  ps-2c  37279  llnmlplnN  37290  lplnle  37291  2atmat  37312  lplnexllnN  37315  2llnjaN  37317  lvoli3  37328  lvoli2  37332  lvolnle3at  37333  islvol2aN  37343  4atlem3  37347  4atlem3a  37348  4atlem3b  37349  4atlem4a  37350  4atlem4b  37351  4atlem4c  37352  4atlem4d  37353  4atlem9  37354  4atlem10a  37355  4atlem10  37357  4atlem11a  37358  4atlem11b  37359  4atlem11  37360  4atlem12a  37361  4atlem12b  37362  4atlem12  37363  4at  37364  4at2  37365  lplncvrlvol2  37366  lplncvrlvol  37367  2lplnja  37370  dalemkelat  37375  lneq2at  37529  lncmp  37534  2lnat  37535  cdlema1N  37542  cdlemblem  37544  cdlemb  37545  paddasslem2  37572  paddasslem5  37575  paddasslem8  37578  paddasslem12  37582  paddasslem13  37583  paddasslem15  37585  pmodlem1  37597  pmodlem2  37598  atmod1i1m  37609  llnmod1i2  37611  llnmod2i2  37614  llnexchb2lem  37619  llnexchb2  37620  dalawlem1  37622  dalawlem2  37623  dalawlem3  37624  dalawlem4  37625  dalawlem5  37626  dalawlem6  37627  dalawlem7  37628  dalawlem8  37629  dalawlem9  37630  dalawlem11  37632  dalawlem12  37633  dalawlem15  37636  pclfinclN  37701  poml4N  37704  osumcllem5N  37711  osumcllem7N  37713  pexmidlem2N  37722  pexmidlem4N  37724  pl42lem1N  37730  pl42lem2N  37731  pl42lem4N  37733  pl42N  37734  lhp2lt  37752  lhpexle2lem  37760  lhpexle3lem  37762  lhpj1  37773  lhpmcvr3  37776  lhpmcvr4N  37777  lhpmcvr5N  37778  lhpmcvr6N  37779  lhp2at0  37783  lhp2atnle  37784  lhpelim  37788  lhpmod2i2  37789  lhpmod6i1  37790  lhprelat3N  37791  lhple  37793  lhpat3  37797  4atexlemkl  37808  ltrnm  37882  ltrnj  37883  ltrnel  37890  ltrncnvel  37893  trljat1  37917  trljat2  37918  trlval3  37938  arglem1N  37941  cdlemc1  37942  cdlemc2  37943  cdlemc4  37945  cdlemc5  37946  cdlemc6  37947  cdlemd2  37950  cdlemd3  37951  cdlemd4  37952  cdlemd7  37955  cdleme0aa  37961  cdleme0b  37963  cdleme0c  37964  cdleme0e  37968  cdleme0fN  37969  cdlemeulpq  37971  cdleme01N  37972  cdleme0ex1N  37974  cdleme3g  37985  cdleme3h  37986  cdleme3  37988  cdleme4a  37990  cdleme5  37991  cdleme7aa  37993  cdleme7c  37996  cdleme7d  37997  cdleme7e  37998  cdleme7ga  37999  cdleme7  38000  cdleme8  38001  cdleme9  38004  cdleme10  38005  cdleme11c  38012  cdleme11e  38014  cdleme11fN  38015  cdleme11g  38016  cdleme11k  38019  cdleme11  38021  cdleme13  38023  cdleme15b  38026  cdleme15d  38028  cdleme15  38029  cdleme16b  38030  cdleme16e  38033  cdleme16f  38034  cdleme17b  38038  cdleme17c  38039  cdleme22gb  38045  cdlemednpq  38050  cdleme19b  38055  cdleme19c  38056  cdleme19e  38058  cdleme20aN  38060  cdleme20bN  38061  cdleme20c  38062  cdleme20d  38063  cdleme20e  38064  cdleme20j  38069  cdleme20k  38070  cdleme20l2  38072  cdleme20l  38073  cdleme20m  38074  cdleme21c  38078  cdleme21ct  38080  cdleme22aa  38090  cdleme22b  38092  cdleme22cN  38093  cdleme22d  38094  cdleme22e  38095  cdleme22eALTN  38096  cdleme22f  38097  cdleme22g  38099  cdleme23a  38100  cdleme23b  38101  cdleme23c  38102  cdleme27N  38120  cdleme28a  38121  cdleme28b  38122  cdleme29ex  38125  cdleme30a  38129  cdlemefr29exN  38153  cdleme32b  38193  cdleme32c  38194  cdleme32e  38196  cdleme35a  38199  cdleme35fnpq  38200  cdleme35b  38201  cdleme35c  38202  cdleme35d  38203  cdleme35f  38205  cdleme42c  38223  cdleme42e  38230  cdleme42h  38233  cdleme42i  38234  cdleme42mgN  38239  cdleme48bw  38253  cdlemeg46frv  38276  cdlemeg46vrg  38278  cdlemeg46rgv  38279  cdlemeg46req  38280  cdleme50eq  38292  cdlemf1  38312  trlord  38320  cdlemg2fv2  38351  cdlemg2m  38355  cdlemg7fvbwN  38358  cdlemg4c  38363  cdlemg4  38368  cdlemg6c  38371  cdlemg8b  38379  cdlemg10bALTN  38387  cdlemg10c  38390  cdlemg10  38392  cdlemg11b  38393  cdlemg12f  38399  cdlemg12g  38400  cdlemg12  38401  cdlemg13a  38402  cdlemg17a  38412  cdlemg17dALTN  38415  cdlemg17  38428  cdlemg18b  38430  cdlemg19a  38434  cdlemg19  38435  cdlemg27a  38443  cdlemg27b  38447  cdlemg31a  38448  cdlemg31b  38449  cdlemg33b0  38452  cdlemg33a  38457  cdlemg35  38464  trlcolem  38477  cdlemg42  38480  cdlemg44a  38482  cdlemg46  38486  trljco  38491  trljco2  38492  tendococl  38523  tendopltp  38531  cdlemh1  38566  cdlemh2  38567  cdlemi1  38569  cdlemi  38571  cdlemk3  38584  cdlemk4  38585  cdlemkvcl  38593  cdlemk10  38594  cdlemk7  38599  cdlemk11  38600  cdlemk12  38601  cdlemkole  38604  cdlemk14  38605  cdlemk15  38606  cdlemk1u  38610  cdlemk5u  38612  cdlemk7u  38621  cdlemk11u  38622  cdlemk12u  38623  cdlemk37  38665  cdlemk39  38667  cdlemkid1  38673  cdlemkid2  38675  cdlemk48  38701  cdlemk50  38703  cdlemk51  38704  cdlemk52  38705  cdlemk39u  38719  dia11N  38799  dia2dimlem1  38815  dia2dimlem2  38816  dia2dimlem3  38817  dia2dimlem10  38824  dia2dimlem12  38826  cdlemm10N  38869  dib11N  38911  diblss  38921  cdlemn2  38946  cdlemn10  38957  dihjustlem  38967  dihord1  38969  dihord2a  38970  dihord2b  38971  dihord2cN  38972  dihord11b  38973  dihord11c  38975  dihord2pre  38976  dihord2pre2  38977  dib2dim  38994  dih2dimb  38995  dihvalcq2  38998  dihopelvalcpre  38999  dihord6apre  39007  dihord5b  39010  dihord6b  39011  dihord5apre  39013  dih11  39016  dihwN  39040  dihmeetlem1N  39041  dihglblem5apreN  39042  dihglblem2N  39045  dihglblem3N  39046  dihmeetlem2N  39050  dihglbcpreN  39051  dihmeetbclemN  39055  dihmeetlem3N  39056  dihmeetlem4preN  39057  dihmeetlem6  39060  dihmeetlem7N  39061  dihjatc1  39062  dihjatc2N  39063  dihjatc3  39064  dihmeetlem9N  39066  dihmeetlem10N  39067  dihmeetlem11N  39068  dihmeetlem15N  39072  dihmeetlem16N  39073  dihmeetlem17N  39074  dihmeetlem19N  39076  dihmeetlem20N  39077  dihmeetALTN  39078  dihmeet2  39097  djhljjN  39153  djhj  39155  dihjatcclem1  39169  dihjatcclem2  39170  dihjatcclem4  39172  dihprrnlem1N  39175  dihprrnlem2  39176  dihjat6  39185  dihjat5N  39188  dvh4dimat  39189