Theorem hllatd 39563

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

Syntax hints:   → wi 4   ∈ wcel 2113  Latclat 18352  HLchlt 39549

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 2115  ax-9 2123  ax-ext 2706

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 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-dm 5632  df-iota 6446  df-fv 6498  df-ov 7359  df-atl 39497  df-cvlat 39521  df-hlat 39550

This theorem is referenced by:  hlrelat  39601  hlrelat2  39602  exatleN  39603  intnatN  39606  hlrelat3  39611  cvrval3  39612  cvrexchlem  39618  lnnat  39626  2atlt  39638  atexchcvrN  39639  atbtwn  39645  4noncolr3  39652  athgt  39655  3dim0  39656  3dimlem3a  39659  3dimlem4a  39662  3dim3  39668  1cvratex  39672  1cvrjat  39674  hlatexch4  39680  ps-2b  39681  3atlem1  39682  3atlem2  39683  3atlem4  39685  3atlem5  39686  3atlem6  39687  2llnmat  39723  2at0mat0  39724  2atm  39726  ps-2c  39727  llnmlplnN  39738  lplnle  39739  2atmat  39760  lplnexllnN  39763  2llnjaN  39765  lvoli3  39776  lvoli2  39780  lvolnle3at  39781  islvol2aN  39791  4atlem3  39795  4atlem3a  39796  4atlem3b  39797  4atlem4a  39798  4atlem4b  39799  4atlem4c  39800  4atlem4d  39801  4atlem9  39802  4atlem10a  39803  4atlem10  39805  4atlem11a  39806  4atlem11b  39807  4atlem11  39808  4atlem12a  39809  4atlem12b  39810  4atlem12  39811  4at  39812  4at2  39813  lplncvrlvol2  39814  lplncvrlvol  39815  2lplnja  39818  dalemkelat  39823  lneq2at  39977  lncmp  39982  2lnat  39983  cdlema1N  39990  cdlemblem  39992  cdlemb  39993  paddasslem2  40020  paddasslem5  40023  paddasslem8  40026  paddasslem12  40030  paddasslem13  40031  paddasslem15  40033  pmodlem1  40045  pmodlem2  40046  atmod1i1m  40057  llnmod1i2  40059  llnmod2i2  40062  llnexchb2lem  40067  llnexchb2  40068  dalawlem1  40070  dalawlem2  40071  dalawlem3  40072  dalawlem4  40073  dalawlem5  40074  dalawlem6  40075  dalawlem7  40076  dalawlem8  40077  dalawlem9  40078  dalawlem11  40080  dalawlem12  40081  dalawlem15  40084  pclfinclN  40149  poml4N  40152  osumcllem5N  40159  osumcllem7N  40161  pexmidlem2N  40170  pexmidlem4N  40172  pl42lem1N  40178  pl42lem2N  40179  pl42lem4N  40181  pl42N  40182  lhp2lt  40200  lhpexle2lem  40208  lhpexle3lem  40210  lhpj1  40221  lhpmcvr3  40224  lhpmcvr4N  40225  lhpmcvr5N  40226  lhpmcvr6N  40227  lhp2at0  40231  lhp2atnle  40232  lhpelim  40236  lhpmod2i2  40237  lhpmod6i1  40238  lhprelat3N  40239  lhple  40241  lhpat3  40245  4atexlemkl  40256  ltrnm  40330  ltrnj  40331  ltrnel  40338  ltrncnvel  40341  trljat1  40365  trljat2  40366  trlval3  40386  arglem1N  40389  cdlemc1  40390  cdlemc2  40391  cdlemc4  40393  cdlemc5  40394  cdlemc6  40395  cdlemd2  40398  cdlemd3  40399  cdlemd4  40400  cdlemd7  40403  cdleme0aa  40409  cdleme0b  40411  cdleme0c  40412  cdleme0e  40416  cdleme0fN  40417  cdlemeulpq  40419  cdleme01N  40420  cdleme0ex1N  40422  cdleme3g  40433  cdleme3h  40434  cdleme3  40436  cdleme4a  40438  cdleme5  40439  cdleme7aa  40441  cdleme7c  40444  cdleme7d  40445  cdleme7e  40446  cdleme7ga  40447  cdleme7  40448  cdleme8  40449  cdleme9  40452  cdleme10  40453  cdleme11c  40460  cdleme11e  40462  cdleme11fN  40463  cdleme11g  40464  cdleme11k  40467  cdleme11  40469  cdleme13  40471  cdleme15b  40474  cdleme15d  40476  cdleme15  40477  cdleme16b  40478  cdleme16e  40481  cdleme16f  40482  cdleme17b  40486  cdleme17c  40487  cdleme22gb  40493  cdlemednpq  40498  cdleme19b  40503  cdleme19c  40504  cdleme19e  40506  cdleme20aN  40508  cdleme20bN  40509  cdleme20c  40510  cdleme20d  40511  cdleme20e  40512  cdleme20j  40517  cdleme20k  40518  cdleme20l2  40520  cdleme20l  40521  cdleme20m  40522  cdleme21c  40526  cdleme21ct  40528  cdleme22aa  40538  cdleme22b  40540  cdleme22cN  40541  cdleme22d  40542  cdleme22e  40543  cdleme22eALTN  40544  cdleme22f  40545  cdleme22g  40547  cdleme23a  40548  cdleme23b  40549  cdleme23c  40550  cdleme27N  40568  cdleme28a  40569  cdleme28b  40570  cdleme29ex  40573  cdleme30a  40577  cdlemefr29exN  40601  cdleme32b  40641  cdleme32c  40642  cdleme32e  40644  cdleme35a  40647  cdleme35fnpq  40648  cdleme35b  40649  cdleme35c  40650  cdleme35d  40651  cdleme35f  40653  cdleme42c  40671  cdleme42e  40678  cdleme42h  40681  cdleme42i  40682  cdleme42mgN  40687  cdleme48bw  40701  cdlemeg46frv  40724  cdlemeg46vrg  40726  cdlemeg46rgv  40727  cdlemeg46req  40728  cdleme50eq  40740  cdlemf1  40760  trlord  40768  cdlemg2fv2  40799  cdlemg2m  40803  cdlemg7fvbwN  40806  cdlemg4c  40811  cdlemg4  40816  cdlemg6c  40819  cdlemg8b  40827  cdlemg10bALTN  40835  cdlemg10c  40838  cdlemg10  40840  cdlemg11b  40841  cdlemg12f  40847  cdlemg12g  40848  cdlemg12  40849  cdlemg13a  40850  cdlemg17a  40860  cdlemg17dALTN  40863  cdlemg17  40876  cdlemg18b  40878  cdlemg19a  40882  cdlemg19  40883  cdlemg27a  40891  cdlemg27b  40895  cdlemg31a  40896  cdlemg31b  40897  cdlemg33b0  40900  cdlemg33a  40905  cdlemg35  40912  trlcolem  40925  cdlemg42  40928  cdlemg44a  40930  cdlemg46  40934  trljco  40939  trljco2  40940  tendococl  40971  tendopltp  40979  cdlemh1  41014  cdlemh2  41015  cdlemi1  41017  cdlemi  41019  cdlemk3  41032  cdlemk4  41033  cdlemkvcl  41041  cdlemk10  41042  cdlemk7  41047  cdlemk11  41048  cdlemk12  41049  cdlemkole  41052  cdlemk14  41053  cdlemk15  41054  cdlemk1u  41058  cdlemk5u  41060  cdlemk7u  41069  cdlemk11u  41070  cdlemk12u  41071  cdlemk37  41113  cdlemk39  41115  cdlemkid1  41121  cdlemkid2  41123  cdlemk48  41149  cdlemk50  41151  cdlemk51  41152  cdlemk52  41153  cdlemk39u  41167  dia11N  41247  dia2dimlem1  41263  dia2dimlem2  41264  dia2dimlem3  41265  dia2dimlem10  41272  dia2dimlem12  41274  cdlemm10N  41317  dib11N  41359  diblss  41369  cdlemn2  41394  cdlemn10  41405  dihjustlem  41415  dihord1  41417  dihord2a  41418  dihord2b  41419  dihord2cN  41420  dihord11b  41421  dihord11c  41423  dihord2pre  41424  dihord2pre2  41425  dib2dim  41442  dih2dimb  41443  dihvalcq2  41446  dihopelvalcpre  41447  dihord6apre  41455  dihord5b  41458  dihord6b  41459  dihord5apre  41461  dih11  41464  dihwN  41488  dihmeetlem1N  41489  dihglblem5apreN  41490  dihglblem2N  41493  dihglblem3N  41494  dihmeetlem2N  41498  dihglbcpreN  41499  dihmeetbclemN  41503  dihmeetlem3N  41504  dihmeetlem4preN  41505  dihmeetlem6  41508  dihmeetlem7N  41509  dihjatc1  41510  dihjatc2N  41511  dihjatc3  41512  dihmeetlem9N  41514  dihmeetlem10N  41515  dihmeetlem11N  41516  dihmeetlem15N  41520  dihmeetlem16N  41521  dihmeetlem17N  41522  dihmeetlem19N  41524  dihmeetlem20N  41525  dihmeetALTN  41526  dihmeet2  41545  djhljjN  41601  djhj  41603  dihjatcclem1  41617  dihjatcclem2  41618  dihjatcclem4  41620  dihprrnlem1N  41623  dihprrnlem2  41624  dihjat6  41633  dihjat5N  41636  dvh4dimat  41637