Theorem hllatd 35981

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

Syntax hints:   → wi 4   ∈ wcel 2079  Latclat 17472  HLchlt 35967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-dm 5445  df-iota 6181  df-fv 6225  df-ov 7010  df-atl 35915  df-cvlat 35939  df-hlat 35968

This theorem is referenced by:  hlrelat  36019  hlrelat2  36020  exatleN  36021  intnatN  36024  hlrelat3  36029  cvrval3  36030  cvrexchlem  36036  lnnat  36044  2atlt  36056  atexchcvrN  36057  atbtwn  36063  4noncolr3  36070  athgt  36073  3dim0  36074  3dimlem3a  36077  3dimlem4a  36080  3dim3  36086  1cvratex  36090  1cvrjat  36092  hlatexch4  36098  ps-2b  36099  3atlem1  36100  3atlem2  36101  3atlem4  36103  3atlem5  36104  3atlem6  36105  2llnmat  36141  2at0mat0  36142  2atm  36144  ps-2c  36145  llnmlplnN  36156  lplnle  36157  2atmat  36178  lplnexllnN  36181  2llnjaN  36183  lvoli3  36194  lvoli2  36198  lvolnle3at  36199  islvol2aN  36209  4atlem3  36213  4atlem3a  36214  4atlem3b  36215  4atlem4a  36216  4atlem4b  36217  4atlem4c  36218  4atlem4d  36219  4atlem9  36220  4atlem10a  36221  4atlem10  36223  4atlem11a  36224  4atlem11b  36225  4atlem11  36226  4atlem12a  36227  4atlem12b  36228  4atlem12  36229  4at  36230  4at2  36231  lplncvrlvol2  36232  lplncvrlvol  36233  2lplnja  36236  dalemkelat  36241  lneq2at  36395  lncmp  36400  2lnat  36401  cdlema1N  36408  cdlemblem  36410  cdlemb  36411  paddasslem2  36438  paddasslem5  36441  paddasslem8  36444  paddasslem12  36448  paddasslem13  36449  paddasslem15  36451  pmodlem1  36463  pmodlem2  36464  atmod1i1m  36475  llnmod1i2  36477  llnmod2i2  36480  llnexchb2lem  36485  llnexchb2  36486  dalawlem1  36488  dalawlem2  36489  dalawlem3  36490  dalawlem4  36491  dalawlem5  36492  dalawlem6  36493  dalawlem7  36494  dalawlem8  36495  dalawlem9  36496  dalawlem11  36498  dalawlem12  36499  dalawlem15  36502  pclfinclN  36567  poml4N  36570  osumcllem5N  36577  osumcllem7N  36579  pexmidlem2N  36588  pexmidlem4N  36590  pl42lem1N  36596  pl42lem2N  36597  pl42lem4N  36599  pl42N  36600  lhp2lt  36618  lhpexle2lem  36626  lhpexle3lem  36628  lhpj1  36639  lhpmcvr3  36642  lhpmcvr4N  36643  lhpmcvr5N  36644  lhpmcvr6N  36645  lhp2at0  36649  lhp2atnle  36650  lhpelim  36654  lhpmod2i2  36655  lhpmod6i1  36656  lhprelat3N  36657  lhple  36659  lhpat3  36663  4atexlemkl  36674  ltrnm  36748  ltrnj  36749  ltrnel  36756  ltrncnvel  36759  trljat1  36783  trljat2  36784  trlval3  36804  arglem1N  36807  cdlemc1  36808  cdlemc2  36809  cdlemc4  36811  cdlemc5  36812  cdlemc6  36813  cdlemd2  36816  cdlemd3  36817  cdlemd4  36818  cdlemd7  36821  cdleme0aa  36827  cdleme0b  36829  cdleme0c  36830  cdleme0e  36834  cdleme0fN  36835  cdlemeulpq  36837  cdleme01N  36838  cdleme0ex1N  36840  cdleme3g  36851  cdleme3h  36852  cdleme3  36854  cdleme4a  36856  cdleme5  36857  cdleme7aa  36859  cdleme7c  36862  cdleme7d  36863  cdleme7e  36864  cdleme7ga  36865  cdleme7  36866  cdleme8  36867  cdleme9  36870  cdleme10  36871  cdleme11c  36878  cdleme11e  36880  cdleme11fN  36881  cdleme11g  36882  cdleme11k  36885  cdleme11  36887  cdleme13  36889  cdleme15b  36892  cdleme15d  36894  cdleme15  36895  cdleme16b  36896  cdleme16e  36899  cdleme16f  36900  cdleme17b  36904  cdleme17c  36905  cdleme22gb  36911  cdlemednpq  36916  cdleme19b  36921  cdleme19c  36922  cdleme19e  36924  cdleme20aN  36926  cdleme20bN  36927  cdleme20c  36928  cdleme20d  36929  cdleme20e  36930  cdleme20j  36935  cdleme20k  36936  cdleme20l2  36938  cdleme20l  36939  cdleme20m  36940  cdleme21c  36944  cdleme21ct  36946  cdleme22aa  36956  cdleme22b  36958  cdleme22cN  36959  cdleme22d  36960  cdleme22e  36961  cdleme22eALTN  36962  cdleme22f  36963  cdleme22g  36965  cdleme23a  36966  cdleme23b  36967  cdleme23c  36968  cdleme27N  36986  cdleme28a  36987  cdleme28b  36988  cdleme29ex  36991  cdleme30a  36995  cdlemefr29exN  37019  cdleme32b  37059  cdleme32c  37060  cdleme32e  37062  cdleme35a  37065  cdleme35fnpq  37066  cdleme35b  37067  cdleme35c  37068  cdleme35d  37069  cdleme35f  37071  cdleme42c  37089  cdleme42e  37096  cdleme42h  37099  cdleme42i  37100  cdleme42mgN  37105  cdleme48bw  37119  cdlemeg46frv  37142  cdlemeg46vrg  37144  cdlemeg46rgv  37145  cdlemeg46req  37146  cdleme50eq  37158  cdlemf1  37178  trlord  37186  cdlemg2fv2  37217  cdlemg2m  37221  cdlemg7fvbwN  37224  cdlemg4c  37229  cdlemg4  37234  cdlemg6c  37237  cdlemg8b  37245  cdlemg10bALTN  37253  cdlemg10c  37256  cdlemg10  37258  cdlemg11b  37259  cdlemg12f  37265  cdlemg12g  37266  cdlemg12  37267  cdlemg13a  37268  cdlemg17a  37278  cdlemg17dALTN  37281  cdlemg17  37294  cdlemg18b  37296  cdlemg19a  37300  cdlemg19  37301  cdlemg27a  37309  cdlemg27b  37313  cdlemg31a  37314  cdlemg31b  37315  cdlemg33b0  37318  cdlemg33a  37323  cdlemg35  37330  trlcolem  37343  cdlemg42  37346  cdlemg44a  37348  cdlemg46  37352  trljco  37357  trljco2  37358  tendococl  37389  tendopltp  37397  cdlemh1  37432  cdlemh2  37433  cdlemi1  37435  cdlemi  37437  cdlemk3  37450  cdlemk4  37451  cdlemkvcl  37459  cdlemk10  37460  cdlemk7  37465  cdlemk11  37466  cdlemk12  37467  cdlemkole  37470  cdlemk14  37471  cdlemk15  37472  cdlemk1u  37476  cdlemk5u  37478  cdlemk7u  37487  cdlemk11u  37488  cdlemk12u  37489  cdlemk37  37531  cdlemk39  37533  cdlemkid1  37539  cdlemkid2  37541  cdlemk48  37567  cdlemk50  37569  cdlemk51  37570  cdlemk52  37571  cdlemk39u  37585  dia11N  37665  dia2dimlem1  37681  dia2dimlem2  37682  dia2dimlem3  37683  dia2dimlem10  37690  dia2dimlem12  37692  cdlemm10N  37735  dib11N  37777  diblss  37787  cdlemn2  37812  cdlemn10  37823  dihjustlem  37833  dihord1  37835  dihord2a  37836  dihord2b  37837  dihord2cN  37838  dihord11b  37839  dihord11c  37841  dihord2pre  37842  dihord2pre2  37843  dib2dim  37860  dih2dimb  37861  dihvalcq2  37864  dihopelvalcpre  37865  dihord6apre  37873  dihord5b  37876  dihord6b  37877  dihord5apre  37879  dih11  37882  dihwN  37906  dihmeetlem1N  37907  dihglblem5apreN  37908  dihglblem2N  37911  dihglblem3N  37912  dihmeetlem2N  37916  dihglbcpreN  37917  dihmeetbclemN  37921  dihmeetlem3N  37922  dihmeetlem4preN  37923  dihmeetlem6  37926  dihmeetlem7N  37927  dihjatc1  37928  dihjatc2N  37929  dihjatc3  37930  dihmeetlem9N  37932  dihmeetlem10N  37933  dihmeetlem11N  37934  dihmeetlem15N  37938  dihmeetlem16N  37939  dihmeetlem17N  37940  dihmeetlem19N  37942  dihmeetlem20N  37943  dihmeetALTN  37944  dihmeet2  37963  djhljjN  38019  djhj  38021  dihjatcclem1  38035  dihjatcclem2  38036  dihjatcclem4  38038  dihprrnlem1N  38041  dihprrnlem2  38042  dihjat6  38051  dihjat5N  38054  dvh4dimat  38055