Theorem hllatd 39473

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

Syntax hints:   → wi 4   ∈ wcel 2111  Latclat 18337  HLchlt 39459

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-dm 5624  df-iota 6437  df-fv 6489  df-ov 7349  df-atl 39407  df-cvlat 39431  df-hlat 39460

This theorem is referenced by:  hlrelat  39511  hlrelat2  39512  exatleN  39513  intnatN  39516  hlrelat3  39521  cvrval3  39522  cvrexchlem  39528  lnnat  39536  2atlt  39548  atexchcvrN  39549  atbtwn  39555  4noncolr3  39562  athgt  39565  3dim0  39566  3dimlem3a  39569  3dimlem4a  39572  3dim3  39578  1cvratex  39582  1cvrjat  39584  hlatexch4  39590  ps-2b  39591  3atlem1  39592  3atlem2  39593  3atlem4  39595  3atlem5  39596  3atlem6  39597  2llnmat  39633  2at0mat0  39634  2atm  39636  ps-2c  39637  llnmlplnN  39648  lplnle  39649  2atmat  39670  lplnexllnN  39673  2llnjaN  39675  lvoli3  39686  lvoli2  39690  lvolnle3at  39691  islvol2aN  39701  4atlem3  39705  4atlem3a  39706  4atlem3b  39707  4atlem4a  39708  4atlem4b  39709  4atlem4c  39710  4atlem4d  39711  4atlem9  39712  4atlem10a  39713  4atlem10  39715  4atlem11a  39716  4atlem11b  39717  4atlem11  39718  4atlem12a  39719  4atlem12b  39720  4atlem12  39721  4at  39722  4at2  39723  lplncvrlvol2  39724  lplncvrlvol  39725  2lplnja  39728  dalemkelat  39733  lneq2at  39887  lncmp  39892  2lnat  39893  cdlema1N  39900  cdlemblem  39902  cdlemb  39903  paddasslem2  39930  paddasslem5  39933  paddasslem8  39936  paddasslem12  39940  paddasslem13  39941  paddasslem15  39943  pmodlem1  39955  pmodlem2  39956  atmod1i1m  39967  llnmod1i2  39969  llnmod2i2  39972  llnexchb2lem  39977  llnexchb2  39978  dalawlem1  39980  dalawlem2  39981  dalawlem3  39982  dalawlem4  39983  dalawlem5  39984  dalawlem6  39985  dalawlem7  39986  dalawlem8  39987  dalawlem9  39988  dalawlem11  39990  dalawlem12  39991  dalawlem15  39994  pclfinclN  40059  poml4N  40062  osumcllem5N  40069  osumcllem7N  40071  pexmidlem2N  40080  pexmidlem4N  40082  pl42lem1N  40088  pl42lem2N  40089  pl42lem4N  40091  pl42N  40092  lhp2lt  40110  lhpexle2lem  40118  lhpexle3lem  40120  lhpj1  40131  lhpmcvr3  40134  lhpmcvr4N  40135  lhpmcvr5N  40136  lhpmcvr6N  40137  lhp2at0  40141  lhp2atnle  40142  lhpelim  40146  lhpmod2i2  40147  lhpmod6i1  40148  lhprelat3N  40149  lhple  40151  lhpat3  40155  4atexlemkl  40166  ltrnm  40240  ltrnj  40241  ltrnel  40248  ltrncnvel  40251  trljat1  40275  trljat2  40276  trlval3  40296  arglem1N  40299  cdlemc1  40300  cdlemc2  40301  cdlemc4  40303  cdlemc5  40304  cdlemc6  40305  cdlemd2  40308  cdlemd3  40309  cdlemd4  40310  cdlemd7  40313  cdleme0aa  40319  cdleme0b  40321  cdleme0c  40322  cdleme0e  40326  cdleme0fN  40327  cdlemeulpq  40329  cdleme01N  40330  cdleme0ex1N  40332  cdleme3g  40343  cdleme3h  40344  cdleme3  40346  cdleme4a  40348  cdleme5  40349  cdleme7aa  40351  cdleme7c  40354  cdleme7d  40355  cdleme7e  40356  cdleme7ga  40357  cdleme7  40358  cdleme8  40359  cdleme9  40362  cdleme10  40363  cdleme11c  40370  cdleme11e  40372  cdleme11fN  40373  cdleme11g  40374  cdleme11k  40377  cdleme11  40379  cdleme13  40381  cdleme15b  40384  cdleme15d  40386  cdleme15  40387  cdleme16b  40388  cdleme16e  40391  cdleme16f  40392  cdleme17b  40396  cdleme17c  40397  cdleme22gb  40403  cdlemednpq  40408  cdleme19b  40413  cdleme19c  40414  cdleme19e  40416  cdleme20aN  40418  cdleme20bN  40419  cdleme20c  40420  cdleme20d  40421  cdleme20e  40422  cdleme20j  40427  cdleme20k  40428  cdleme20l2  40430  cdleme20l  40431  cdleme20m  40432  cdleme21c  40436  cdleme21ct  40438  cdleme22aa  40448  cdleme22b  40450  cdleme22cN  40451  cdleme22d  40452  cdleme22e  40453  cdleme22eALTN  40454  cdleme22f  40455  cdleme22g  40457  cdleme23a  40458  cdleme23b  40459  cdleme23c  40460  cdleme27N  40478  cdleme28a  40479  cdleme28b  40480  cdleme29ex  40483  cdleme30a  40487  cdlemefr29exN  40511  cdleme32b  40551  cdleme32c  40552  cdleme32e  40554  cdleme35a  40557  cdleme35fnpq  40558  cdleme35b  40559  cdleme35c  40560  cdleme35d  40561  cdleme35f  40563  cdleme42c  40581  cdleme42e  40588  cdleme42h  40591  cdleme42i  40592  cdleme42mgN  40597  cdleme48bw  40611  cdlemeg46frv  40634  cdlemeg46vrg  40636  cdlemeg46rgv  40637  cdlemeg46req  40638  cdleme50eq  40650  cdlemf1  40670  trlord  40678  cdlemg2fv2  40709  cdlemg2m  40713  cdlemg7fvbwN  40716  cdlemg4c  40721  cdlemg4  40726  cdlemg6c  40729  cdlemg8b  40737  cdlemg10bALTN  40745  cdlemg10c  40748  cdlemg10  40750  cdlemg11b  40751  cdlemg12f  40757  cdlemg12g  40758  cdlemg12  40759  cdlemg13a  40760  cdlemg17a  40770  cdlemg17dALTN  40773  cdlemg17  40786  cdlemg18b  40788  cdlemg19a  40792  cdlemg19  40793  cdlemg27a  40801  cdlemg27b  40805  cdlemg31a  40806  cdlemg31b  40807  cdlemg33b0  40810  cdlemg33a  40815  cdlemg35  40822  trlcolem  40835  cdlemg42  40838  cdlemg44a  40840  cdlemg46  40844  trljco  40849  trljco2  40850  tendococl  40881  tendopltp  40889  cdlemh1  40924  cdlemh2  40925  cdlemi1  40927  cdlemi  40929  cdlemk3  40942  cdlemk4  40943  cdlemkvcl  40951  cdlemk10  40952  cdlemk7  40957  cdlemk11  40958  cdlemk12  40959  cdlemkole  40962  cdlemk14  40963  cdlemk15  40964  cdlemk1u  40968  cdlemk5u  40970  cdlemk7u  40979  cdlemk11u  40980  cdlemk12u  40981  cdlemk37  41023  cdlemk39  41025  cdlemkid1  41031  cdlemkid2  41033  cdlemk48  41059  cdlemk50  41061  cdlemk51  41062  cdlemk52  41063  cdlemk39u  41077  dia11N  41157  dia2dimlem1  41173  dia2dimlem2  41174  dia2dimlem3  41175  dia2dimlem10  41182  dia2dimlem12  41184  cdlemm10N  41227  dib11N  41269  diblss  41279  cdlemn2  41304  cdlemn10  41315  dihjustlem  41325  dihord1  41327  dihord2a  41328  dihord2b  41329  dihord2cN  41330  dihord11b  41331  dihord11c  41333  dihord2pre  41334  dihord2pre2  41335  dib2dim  41352  dih2dimb  41353  dihvalcq2  41356  dihopelvalcpre  41357  dihord6apre  41365  dihord5b  41368  dihord6b  41369  dihord5apre  41371  dih11  41374  dihwN  41398  dihmeetlem1N  41399  dihglblem5apreN  41400  dihglblem2N  41403  dihglblem3N  41404  dihmeetlem2N  41408  dihglbcpreN  41409  dihmeetbclemN  41413  dihmeetlem3N  41414  dihmeetlem4preN  41415  dihmeetlem6  41418  dihmeetlem7N  41419  dihjatc1  41420  dihjatc2N  41421  dihjatc3  41422  dihmeetlem9N  41424  dihmeetlem10N  41425  dihmeetlem11N  41426  dihmeetlem15N  41430  dihmeetlem16N  41431  dihmeetlem17N  41432  dihmeetlem19N  41434  dihmeetlem20N  41435  dihmeetALTN  41436  dihmeet2  41455  djhljjN  41511  djhj  41513  dihjatcclem1  41527  dihjatcclem2  41528  dihjatcclem4  41530  dihprrnlem1N  41533  dihprrnlem2  41534  dihjat6  41543  dihjat5N  41546  dvh4dimat  41547