Theorem hllatd 39064

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

Syntax hints:   → wi 4   ∈ wcel 2099  Latclat 18458  HLchlt 39050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4916  df-br 5156  df-dm 5694  df-iota 6508  df-fv 6564  df-ov 7429  df-atl 38998  df-cvlat 39022  df-hlat 39051

This theorem is referenced by:  hlrelat  39103  hlrelat2  39104  exatleN  39105  intnatN  39108  hlrelat3  39113  cvrval3  39114  cvrexchlem  39120  lnnat  39128  2atlt  39140  atexchcvrN  39141  atbtwn  39147  4noncolr3  39154  athgt  39157  3dim0  39158  3dimlem3a  39161  3dimlem4a  39164  3dim3  39170  1cvratex  39174  1cvrjat  39176  hlatexch4  39182  ps-2b  39183  3atlem1  39184  3atlem2  39185  3atlem4  39187  3atlem5  39188  3atlem6  39189  2llnmat  39225  2at0mat0  39226  2atm  39228  ps-2c  39229  llnmlplnN  39240  lplnle  39241  2atmat  39262  lplnexllnN  39265  2llnjaN  39267  lvoli3  39278  lvoli2  39282  lvolnle3at  39283  islvol2aN  39293  4atlem3  39297  4atlem3a  39298  4atlem3b  39299  4atlem4a  39300  4atlem4b  39301  4atlem4c  39302  4atlem4d  39303  4atlem9  39304  4atlem10a  39305  4atlem10  39307  4atlem11a  39308  4atlem11b  39309  4atlem11  39310  4atlem12a  39311  4atlem12b  39312  4atlem12  39313  4at  39314  4at2  39315  lplncvrlvol2  39316  lplncvrlvol  39317  2lplnja  39320  dalemkelat  39325  lneq2at  39479  lncmp  39484  2lnat  39485  cdlema1N  39492  cdlemblem  39494  cdlemb  39495  paddasslem2  39522  paddasslem5  39525  paddasslem8  39528  paddasslem12  39532  paddasslem13  39533  paddasslem15  39535  pmodlem1  39547  pmodlem2  39548  atmod1i1m  39559  llnmod1i2  39561  llnmod2i2  39564  llnexchb2lem  39569  llnexchb2  39570  dalawlem1  39572  dalawlem2  39573  dalawlem3  39574  dalawlem4  39575  dalawlem5  39576  dalawlem6  39577  dalawlem7  39578  dalawlem8  39579  dalawlem9  39580  dalawlem11  39582  dalawlem12  39583  dalawlem15  39586  pclfinclN  39651  poml4N  39654  osumcllem5N  39661  osumcllem7N  39663  pexmidlem2N  39672  pexmidlem4N  39674  pl42lem1N  39680  pl42lem2N  39681  pl42lem4N  39683  pl42N  39684  lhp2lt  39702  lhpexle2lem  39710  lhpexle3lem  39712  lhpj1  39723  lhpmcvr3  39726  lhpmcvr4N  39727  lhpmcvr5N  39728  lhpmcvr6N  39729  lhp2at0  39733  lhp2atnle  39734  lhpelim  39738  lhpmod2i2  39739  lhpmod6i1  39740  lhprelat3N  39741  lhple  39743  lhpat3  39747  4atexlemkl  39758  ltrnm  39832  ltrnj  39833  ltrnel  39840  ltrncnvel  39843  trljat1  39867  trljat2  39868  trlval3  39888  arglem1N  39891  cdlemc1  39892  cdlemc2  39893  cdlemc4  39895  cdlemc5  39896  cdlemc6  39897  cdlemd2  39900  cdlemd3  39901  cdlemd4  39902  cdlemd7  39905  cdleme0aa  39911  cdleme0b  39913  cdleme0c  39914  cdleme0e  39918  cdleme0fN  39919  cdlemeulpq  39921  cdleme01N  39922  cdleme0ex1N  39924  cdleme3g  39935  cdleme3h  39936  cdleme3  39938  cdleme4a  39940  cdleme5  39941  cdleme7aa  39943  cdleme7c  39946  cdleme7d  39947  cdleme7e  39948  cdleme7ga  39949  cdleme7  39950  cdleme8  39951  cdleme9  39954  cdleme10  39955  cdleme11c  39962  cdleme11e  39964  cdleme11fN  39965  cdleme11g  39966  cdleme11k  39969  cdleme11  39971  cdleme13  39973  cdleme15b  39976  cdleme15d  39978  cdleme15  39979  cdleme16b  39980  cdleme16e  39983  cdleme16f  39984  cdleme17b  39988  cdleme17c  39989  cdleme22gb  39995  cdlemednpq  40000  cdleme19b  40005  cdleme19c  40006  cdleme19e  40008  cdleme20aN  40010  cdleme20bN  40011  cdleme20c  40012  cdleme20d  40013  cdleme20e  40014  cdleme20j  40019  cdleme20k  40020  cdleme20l2  40022  cdleme20l  40023  cdleme20m  40024  cdleme21c  40028  cdleme21ct  40030  cdleme22aa  40040  cdleme22b  40042  cdleme22cN  40043  cdleme22d  40044  cdleme22e  40045  cdleme22eALTN  40046  cdleme22f  40047  cdleme22g  40049  cdleme23a  40050  cdleme23b  40051  cdleme23c  40052  cdleme27N  40070  cdleme28a  40071  cdleme28b  40072  cdleme29ex  40075  cdleme30a  40079  cdlemefr29exN  40103  cdleme32b  40143  cdleme32c  40144  cdleme32e  40146  cdleme35a  40149  cdleme35fnpq  40150  cdleme35b  40151  cdleme35c  40152  cdleme35d  40153  cdleme35f  40155  cdleme42c  40173  cdleme42e  40180  cdleme42h  40183  cdleme42i  40184  cdleme42mgN  40189  cdleme48bw  40203  cdlemeg46frv  40226  cdlemeg46vrg  40228  cdlemeg46rgv  40229  cdlemeg46req  40230  cdleme50eq  40242  cdlemf1  40262  trlord  40270  cdlemg2fv2  40301  cdlemg2m  40305  cdlemg7fvbwN  40308  cdlemg4c  40313  cdlemg4  40318  cdlemg6c  40321  cdlemg8b  40329  cdlemg10bALTN  40337  cdlemg10c  40340  cdlemg10  40342  cdlemg11b  40343  cdlemg12f  40349  cdlemg12g  40350  cdlemg12  40351  cdlemg13a  40352  cdlemg17a  40362  cdlemg17dALTN  40365  cdlemg17  40378  cdlemg18b  40380  cdlemg19a  40384  cdlemg19  40385  cdlemg27a  40393  cdlemg27b  40397  cdlemg31a  40398  cdlemg31b  40399  cdlemg33b0  40402  cdlemg33a  40407  cdlemg35  40414  trlcolem  40427  cdlemg42  40430  cdlemg44a  40432  cdlemg46  40436  trljco  40441  trljco2  40442  tendococl  40473  tendopltp  40481  cdlemh1  40516  cdlemh2  40517  cdlemi1  40519  cdlemi  40521  cdlemk3  40534  cdlemk4  40535  cdlemkvcl  40543  cdlemk10  40544  cdlemk7  40549  cdlemk11  40550  cdlemk12  40551  cdlemkole  40554  cdlemk14  40555  cdlemk15  40556  cdlemk1u  40560  cdlemk5u  40562  cdlemk7u  40571  cdlemk11u  40572  cdlemk12u  40573  cdlemk37  40615  cdlemk39  40617  cdlemkid1  40623  cdlemkid2  40625  cdlemk48  40651  cdlemk50  40653  cdlemk51  40654  cdlemk52  40655  cdlemk39u  40669  dia11N  40749  dia2dimlem1  40765  dia2dimlem2  40766  dia2dimlem3  40767  dia2dimlem10  40774  dia2dimlem12  40776  cdlemm10N  40819  dib11N  40861  diblss  40871  cdlemn2  40896  cdlemn10  40907  dihjustlem  40917  dihord1  40919  dihord2a  40920  dihord2b  40921  dihord2cN  40922  dihord11b  40923  dihord11c  40925  dihord2pre  40926  dihord2pre2  40927  dib2dim  40944  dih2dimb  40945  dihvalcq2  40948  dihopelvalcpre  40949  dihord6apre  40957  dihord5b  40960  dihord6b  40961  dihord5apre  40963  dih11  40966  dihwN  40990  dihmeetlem1N  40991  dihglblem5apreN  40992  dihglblem2N  40995  dihglblem3N  40996  dihmeetlem2N  41000  dihglbcpreN  41001  dihmeetbclemN  41005  dihmeetlem3N  41006  dihmeetlem4preN  41007  dihmeetlem6  41010  dihmeetlem7N  41011  dihjatc1  41012  dihjatc2N  41013  dihjatc3  41014  dihmeetlem9N  41016  dihmeetlem10N  41017  dihmeetlem11N  41018  dihmeetlem15N  41022  dihmeetlem16N  41023  dihmeetlem17N  41024  dihmeetlem19N  41026  dihmeetlem20N  41027  dihmeetALTN  41028  dihmeet2  41047  djhljjN  41103  djhj  41105  dihjatcclem1  41119  dihjatcclem2  41120  dihjatcclem4  41122  dihprrnlem1N  41125  dihprrnlem2  41126  dihjat6  41135  dihjat5N  41138  dvh4dimat  41139