Theorem hllatd 39856

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

Syntax hints:   → wi 4   ∈ wcel 2119  Latclat 18388  HLchlt 39842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-dm 5628  df-iota 6441  df-fv 6493  df-ov 7359  df-atl 39790  df-cvlat 39814  df-hlat 39843

This theorem is referenced by:  hlrelat  39894  hlrelat2  39895  exatleN  39896  intnatN  39899  hlrelat3  39904  cvrval3  39905  cvrexchlem  39911  lnnat  39919  2atlt  39931  atexchcvrN  39932  atbtwn  39938  4noncolr3  39945  athgt  39948  3dim0  39949  3dimlem3a  39952  3dimlem4a  39955  3dim3  39961  1cvratex  39965  1cvrjat  39967  hlatexch4  39973  ps-2b  39974  3atlem1  39975  3atlem2  39976  3atlem4  39978  3atlem5  39979  3atlem6  39980  2llnmat  40016  2at0mat0  40017  2atm  40019  ps-2c  40020  llnmlplnN  40031  lplnle  40032  2atmat  40053  lplnexllnN  40056  2llnjaN  40058  lvoli3  40069  lvoli2  40073  lvolnle3at  40074  islvol2aN  40084  4atlem3  40088  4atlem3a  40089  4atlem3b  40090  4atlem4a  40091  4atlem4b  40092  4atlem4c  40093  4atlem4d  40094  4atlem9  40095  4atlem10a  40096  4atlem10  40098  4atlem11a  40099  4atlem11b  40100  4atlem11  40101  4atlem12a  40102  4atlem12b  40103  4atlem12  40104  4at  40105  4at2  40106  lplncvrlvol2  40107  lplncvrlvol  40108  2lplnja  40111  dalemkelat  40116  lneq2at  40270  lncmp  40275  2lnat  40276  cdlema1N  40283  cdlemblem  40285  cdlemb  40286  paddasslem2  40313  paddasslem5  40316  paddasslem8  40319  paddasslem12  40323  paddasslem13  40324  paddasslem15  40326  pmodlem1  40338  pmodlem2  40339  atmod1i1m  40350  llnmod1i2  40352  llnmod2i2  40355  llnexchb2lem  40360  llnexchb2  40361  dalawlem1  40363  dalawlem2  40364  dalawlem3  40365  dalawlem4  40366  dalawlem5  40367  dalawlem6  40368  dalawlem7  40369  dalawlem8  40370  dalawlem9  40371  dalawlem11  40373  dalawlem12  40374  dalawlem15  40377  pclfinclN  40442  poml4N  40445  osumcllem5N  40452  osumcllem7N  40454  pexmidlem2N  40463  pexmidlem4N  40465  pl42lem1N  40471  pl42lem2N  40472  pl42lem4N  40474  pl42N  40475  lhp2lt  40493  lhpexle2lem  40501  lhpexle3lem  40503  lhpj1  40514  lhpmcvr3  40517  lhpmcvr4N  40518  lhpmcvr5N  40519  lhpmcvr6N  40520  lhp2at0  40524  lhp2atnle  40525  lhpelim  40529  lhpmod2i2  40530  lhpmod6i1  40531  lhprelat3N  40532  lhple  40534  lhpat3  40538  4atexlemkl  40549  ltrnm  40623  ltrnj  40624  ltrnel  40631  ltrncnvel  40634  trljat1  40658  trljat2  40659  trlval3  40679  arglem1N  40682  cdlemc1  40683  cdlemc2  40684  cdlemc4  40686  cdlemc5  40687  cdlemc6  40688  cdlemd2  40691  cdlemd3  40692  cdlemd4  40693  cdlemd7  40696  cdleme0aa  40702  cdleme0b  40704  cdleme0c  40705  cdleme0e  40709  cdleme0fN  40710  cdlemeulpq  40712  cdleme01N  40713  cdleme0ex1N  40715  cdleme3g  40726  cdleme3h  40727  cdleme3  40729  cdleme4a  40731  cdleme5  40732  cdleme7aa  40734  cdleme7c  40737  cdleme7d  40738  cdleme7e  40739  cdleme7ga  40740  cdleme7  40741  cdleme8  40742  cdleme9  40745  cdleme10  40746  cdleme11c  40753  cdleme11e  40755  cdleme11fN  40756  cdleme11g  40757  cdleme11k  40760  cdleme11  40762  cdleme13  40764  cdleme15b  40767  cdleme15d  40769  cdleme15  40770  cdleme16b  40771  cdleme16e  40774  cdleme16f  40775  cdleme17b  40779  cdleme17c  40780  cdleme22gb  40786  cdlemednpq  40791  cdleme19b  40796  cdleme19c  40797  cdleme19e  40799  cdleme20aN  40801  cdleme20bN  40802  cdleme20c  40803  cdleme20d  40804  cdleme20e  40805  cdleme20j  40810  cdleme20k  40811  cdleme20l2  40813  cdleme20l  40814  cdleme20m  40815  cdleme21c  40819  cdleme21ct  40821  cdleme22aa  40831  cdleme22b  40833  cdleme22cN  40834  cdleme22d  40835  cdleme22e  40836  cdleme22eALTN  40837  cdleme22f  40838  cdleme22g  40840  cdleme23a  40841  cdleme23b  40842  cdleme23c  40843  cdleme27N  40861  cdleme28a  40862  cdleme28b  40863  cdleme29ex  40866  cdleme30a  40870  cdlemefr29exN  40894  cdleme32b  40934  cdleme32c  40935  cdleme32e  40937  cdleme35a  40940  cdleme35fnpq  40941  cdleme35b  40942  cdleme35c  40943  cdleme35d  40944  cdleme35f  40946  cdleme42c  40964  cdleme42e  40971  cdleme42h  40974  cdleme42i  40975  cdleme42mgN  40980  cdleme48bw  40994  cdlemeg46frv  41017  cdlemeg46vrg  41019  cdlemeg46rgv  41020  cdlemeg46req  41021  cdleme50eq  41033  cdlemf1  41053  trlord  41061  cdlemg2fv2  41092  cdlemg2m  41096  cdlemg7fvbwN  41099  cdlemg4c  41104  cdlemg4  41109  cdlemg6c  41112  cdlemg8b  41120  cdlemg10bALTN  41128  cdlemg10c  41131  cdlemg10  41133  cdlemg11b  41134  cdlemg12f  41140  cdlemg12g  41141  cdlemg12  41142  cdlemg13a  41143  cdlemg17a  41153  cdlemg17dALTN  41156  cdlemg17  41169  cdlemg18b  41171  cdlemg19a  41175  cdlemg19  41176  cdlemg27a  41184  cdlemg27b  41188  cdlemg31a  41189  cdlemg31b  41190  cdlemg33b0  41193  cdlemg33a  41198  cdlemg35  41205  trlcolem  41218  cdlemg42  41221  cdlemg44a  41223  cdlemg46  41227  trljco  41232  trljco2  41233  tendococl  41264  tendopltp  41272  cdlemh1  41307  cdlemh2  41308  cdlemi1  41310  cdlemi  41312  cdlemk3  41325  cdlemk4  41326  cdlemkvcl  41334  cdlemk10  41335  cdlemk7  41340  cdlemk11  41341  cdlemk12  41342  cdlemkole  41345  cdlemk14  41346  cdlemk15  41347  cdlemk1u  41351  cdlemk5u  41353  cdlemk7u  41362  cdlemk11u  41363  cdlemk12u  41364  cdlemk37  41406  cdlemk39  41408  cdlemkid1  41414  cdlemkid2  41416  cdlemk48  41442  cdlemk50  41444  cdlemk51  41445  cdlemk52  41446  cdlemk39u  41460  dia11N  41540  dia2dimlem1  41556  dia2dimlem2  41557  dia2dimlem3  41558  dia2dimlem10  41565  dia2dimlem12  41567  cdlemm10N  41610  dib11N  41652  diblss  41662  cdlemn2  41687  cdlemn10  41698  dihjustlem  41708  dihord1  41710  dihord2a  41711  dihord2b  41712  dihord2cN  41713  dihord11b  41714  dihord11c  41716  dihord2pre  41717  dihord2pre2  41718  dib2dim  41735  dih2dimb  41736  dihvalcq2  41739  dihopelvalcpre  41740  dihord6apre  41748  dihord5b  41751  dihord6b  41752  dihord5apre  41754  dih11  41757  dihwN  41781  dihmeetlem1N  41782  dihglblem5apreN  41783  dihglblem2N  41786  dihglblem3N  41787  dihmeetlem2N  41791  dihglbcpreN  41792  dihmeetbclemN  41796  dihmeetlem3N  41797  dihmeetlem4preN  41798  dihmeetlem6  41801  dihmeetlem7N  41802  dihjatc1  41803  dihjatc2N  41804  dihjatc3  41805  dihmeetlem9N  41807  dihmeetlem10N  41808  dihmeetlem11N  41809  dihmeetlem15N  41813  dihmeetlem16N  41814  dihmeetlem17N  41815  dihmeetlem19N  41817  dihmeetlem20N  41818  dihmeetALTN  41819  dihmeet2  41838  djhljjN  41894  djhj  41896  dihjatcclem1  41910  dihjatcclem2  41911  dihjatcclem4  41913  dihprrnlem1N  41916  dihprrnlem2  41917  dihjat6  41926  dihjat5N  41929  dvh4dimat  41930