Theorem hllatd 40166

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143  Latclat 18491  HLchlt 40152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-dm 5671  df-iota 6492  df-fv 6544  df-ov 7413  df-atl 40100  df-cvlat 40124  df-hlat 40153

This theorem is used by:  hlrelat  40204  hlrelat2  40205  exatleN  40206  intnatN  40209  hlrelat3  40214  cvrval3  40215  cvrexchlem  40221  lnnat  40229  2atlt  40241  atexchcvrN  40242  atbtwn  40248  4noncolr3  40255  athgt  40258  3dim0  40259  3dimlem3a  40262  3dimlem4a  40265  3dim3  40271  1cvratex  40275  1cvrjat  40277  hlatexch4  40283  ps-2b  40284  3atlem1  40285  3atlem2  40286  3atlem4  40288  3atlem5  40289  3atlem6  40290  2llnmat  40326  2at0mat0  40327  2atm  40329  ps-2c  40330  llnmlplnN  40341  lplnle  40342  2atmat  40363  lplnexllnN  40366  2llnjaN  40368  lvoli3  40379  lvoli2  40383  lvolnle3at  40384  islvol2aN  40394  4atlem3  40398  4atlem3a  40399  4atlem3b  40400  4atlem4a  40401  4atlem4b  40402  4atlem4c  40403  4atlem4d  40404  4atlem9  40405  4atlem10a  40406  4atlem10  40408  4atlem11a  40409  4atlem11b  40410  4atlem11  40411  4atlem12a  40412  4atlem12b  40413  4atlem12  40414  4at  40415  4at2  40416  lplncvrlvol2  40417  lplncvrlvol  40418  2lplnja  40421  dalemkelat  40426  lneq2at  40580  lncmp  40585  2lnat  40586  cdlema1N  40593  cdlemblem  40595  cdlemb  40596  paddasslem2  40623  paddasslem5  40626  paddasslem8  40629  paddasslem12  40633  paddasslem13  40634  paddasslem15  40636  pmodlem1  40648  pmodlem2  40649  atmod1i1m  40660  llnmod1i2  40662  llnmod2i2  40665  llnexchb2lem  40670  llnexchb2  40671  dalawlem1  40673  dalawlem2  40674  dalawlem3  40675  dalawlem4  40676  dalawlem5  40677  dalawlem6  40678  dalawlem7  40679  dalawlem8  40680  dalawlem9  40681  dalawlem11  40683  dalawlem12  40684  dalawlem15  40687  pclfinclN  40752  poml4N  40755  osumcllem5N  40762  osumcllem7N  40764  pexmidlem2N  40773  pexmidlem4N  40775  pl42lem1N  40781  pl42lem2N  40782  pl42lem4N  40784  pl42N  40785  lhp2lt  40803  lhpexle2lem  40811  lhpexle3lem  40813  lhpj1  40824  lhpmcvr3  40827  lhpmcvr4N  40828  lhpmcvr5N  40829  lhpmcvr6N  40830  lhp2at0  40834  lhp2atnle  40835  lhpelim  40839  lhpmod2i2  40840  lhpmod6i1  40841  lhprelat3N  40842  lhple  40844  lhpat3  40848  4atexlemkl  40859  ltrnm  40933  ltrnj  40934  ltrnel  40941  ltrncnvel  40944  trljat1  40968  trljat2  40969  trlval3  40989  arglem1N  40992  cdlemc1  40993  cdlemc2  40994  cdlemc4  40996  cdlemc5  40997  cdlemc6  40998  cdlemd2  41001  cdlemd3  41002  cdlemd4  41003  cdlemd7  41006  cdleme0aa  41012  cdleme0b  41014  cdleme0c  41015  cdleme0e  41019  cdleme0fN  41020  cdlemeulpq  41022  cdleme01N  41023  cdleme0ex1N  41025  cdleme3g  41036  cdleme3h  41037  cdleme3  41039  cdleme4a  41041  cdleme5  41042  cdleme7aa  41044  cdleme7c  41047  cdleme7d  41048  cdleme7e  41049  cdleme7ga  41050  cdleme7  41051  cdleme8  41052  cdleme9  41055  cdleme10  41056  cdleme11c  41063  cdleme11e  41065  cdleme11fN  41066  cdleme11g  41067  cdleme11k  41070  cdleme11  41072  cdleme13  41074  cdleme15b  41077  cdleme15d  41079  cdleme15  41080  cdleme16b  41081  cdleme16e  41084  cdleme16f  41085  cdleme17b  41089  cdleme17c  41090  cdleme22gb  41096  cdlemednpq  41101  cdleme19b  41106  cdleme19c  41107  cdleme19e  41109  cdleme20aN  41111  cdleme20bN  41112  cdleme20c  41113  cdleme20d  41114  cdleme20e  41115  cdleme20j  41120  cdleme20k  41121  cdleme20l2  41123  cdleme20l  41124  cdleme20m  41125  cdleme21c  41129  cdleme21ct  41131  cdleme22aa  41141  cdleme22b  41143  cdleme22cN  41144  cdleme22d  41145  cdleme22e  41146  cdleme22eALTN  41147  cdleme22f  41148  cdleme22g  41150  cdleme23a  41151  cdleme23b  41152  cdleme23c  41153  cdleme27N  41171  cdleme28a  41172  cdleme28b  41173  cdleme29ex  41176  cdleme30a  41180  cdlemefr29exN  41204  cdleme32b  41244  cdleme32c  41245  cdleme32e  41247  cdleme35a  41250  cdleme35fnpq  41251  cdleme35b  41252  cdleme35c  41253  cdleme35d  41254  cdleme35f  41256  cdleme42c  41274  cdleme42e  41281  cdleme42h  41284  cdleme42i  41285  cdleme42mgN  41290  cdleme48bw  41304  cdlemeg46frv  41327  cdlemeg46vrg  41329  cdlemeg46rgv  41330  cdlemeg46req  41331  cdleme50eq  41343  cdlemf1  41363  trlord  41371  cdlemg2fv2  41402  cdlemg2m  41406  cdlemg7fvbwN  41409  cdlemg4c  41414  cdlemg4  41419  cdlemg6c  41422  cdlemg8b  41430  cdlemg10bALTN  41438  cdlemg10c  41441  cdlemg10  41443  cdlemg11b  41444  cdlemg12f  41450  cdlemg12g  41451  cdlemg12  41452  cdlemg13a  41453  cdlemg17a  41463  cdlemg17dALTN  41466  cdlemg17  41479  cdlemg18b  41481  cdlemg19a  41485  cdlemg19  41486  cdlemg27a  41494  cdlemg27b  41498  cdlemg31a  41499  cdlemg31b  41500  cdlemg33b0  41503  cdlemg33a  41508  cdlemg35  41515  trlcolem  41528  cdlemg42  41531  cdlemg44a  41533  cdlemg46  41537  trljco  41542  trljco2  41543  tendococl  41574  tendopltp  41582  cdlemh1  41617  cdlemh2  41618  cdlemi1  41620  cdlemi  41622  cdlemk3  41635  cdlemk4  41636  cdlemkvcl  41644  cdlemk10  41645  cdlemk7  41650  cdlemk11  41651  cdlemk12  41652  cdlemkole  41655  cdlemk14  41656  cdlemk15  41657  cdlemk1u  41661  cdlemk5u  41663  cdlemk7u  41672  cdlemk11u  41673  cdlemk12u  41674  cdlemk37  41716  cdlemk39  41718  cdlemkid1  41724  cdlemkid2  41726  cdlemk48  41752  cdlemk50  41754  cdlemk51  41755  cdlemk52  41756  cdlemk39u  41770  dia11N  41850  dia2dimlem1  41866  dia2dimlem2  41867  dia2dimlem3  41868  dia2dimlem10  41875  dia2dimlem12  41877  cdlemm10N  41920  dib11N  41962  diblss  41972  cdlemn2  41997  cdlemn10  42008  dihjustlem  42018  dihord1  42020  dihord2a  42021  dihord2b  42022  dihord2cN  42023  dihord11b  42024  dihord11c  42026  dihord2pre  42027  dihord2pre2  42028  dib2dim  42045  dih2dimb  42046  dihvalcq2  42049  dihopelvalcpre  42050  dihord6apre  42058  dihord5b  42061  dihord6b  42062  dihord5apre  42064  dih11  42067  dihwN  42091  dihmeetlem1N  42092  dihglblem5apreN  42093  dihglblem2N  42096  dihglblem3N  42097  dihmeetlem2N  42101  dihglbcpreN  42102  dihmeetbclemN  42106  dihmeetlem3N  42107  dihmeetlem4preN  42108  dihmeetlem6  42111  dihmeetlem7N  42112  dihjatc1  42113  dihjatc2N  42114  dihjatc3  42115  dihmeetlem9N  42117  dihmeetlem10N  42118  dihmeetlem11N  42119  dihmeetlem15N  42123  dihmeetlem16N  42124  dihmeetlem17N  42125  dihmeetlem19N  42127  dihmeetlem20N  42128  dihmeetALTN  42129  dihmeet2  42148  djhljjN  42204  djhj  42206  dihjatcclem1  42220  dihjatcclem2  42221  dihjatcclem4  42223  dihprrnlem1N  42226  dihprrnlem2  42227  dihjat6  42236  dihjat5N  42239  dvh4dimat  42240