Theorem hllatd 40028

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

Syntax hints:   → wi 4   ∈ wcel 2149  Latclat 18487  HLchlt 40014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-dm 5672  df-iota 6493  df-fv 6545  df-ov 7414  df-atl 39962  df-cvlat 39986  df-hlat 40015

This theorem is referenced by:  hlrelat  40066  hlrelat2  40067  exatleN  40068  intnatN  40071  hlrelat3  40076  cvrval3  40077  cvrexchlem  40083  lnnat  40091  2atlt  40103  atexchcvrN  40104  atbtwn  40110  4noncolr3  40117  athgt  40120  3dim0  40121  3dimlem3a  40124  3dimlem4a  40127  3dim3  40133  1cvratex  40137  1cvrjat  40139  hlatexch4  40145  ps-2b  40146  3atlem1  40147  3atlem2  40148  3atlem4  40150  3atlem5  40151  3atlem6  40152  2llnmat  40188  2at0mat0  40189  2atm  40191  ps-2c  40192  llnmlplnN  40203  lplnle  40204  2atmat  40225  lplnexllnN  40228  2llnjaN  40230  lvoli3  40241  lvoli2  40245  lvolnle3at  40246  islvol2aN  40256  4atlem3  40260  4atlem3a  40261  4atlem3b  40262  4atlem4a  40263  4atlem4b  40264  4atlem4c  40265  4atlem4d  40266  4atlem9  40267  4atlem10a  40268  4atlem10  40270  4atlem11a  40271  4atlem11b  40272  4atlem11  40273  4atlem12a  40274  4atlem12b  40275  4atlem12  40276  4at  40277  4at2  40278  lplncvrlvol2  40279  lplncvrlvol  40280  2lplnja  40283  dalemkelat  40288  lneq2at  40442  lncmp  40447  2lnat  40448  cdlema1N  40455  cdlemblem  40457  cdlemb  40458  paddasslem2  40485  paddasslem5  40488  paddasslem8  40491  paddasslem12  40495  paddasslem13  40496  paddasslem15  40498  pmodlem1  40510  pmodlem2  40511  atmod1i1m  40522  llnmod1i2  40524  llnmod2i2  40527  llnexchb2lem  40532  llnexchb2  40533  dalawlem1  40535  dalawlem2  40536  dalawlem3  40537  dalawlem4  40538  dalawlem5  40539  dalawlem6  40540  dalawlem7  40541  dalawlem8  40542  dalawlem9  40543  dalawlem11  40545  dalawlem12  40546  dalawlem15  40549  pclfinclN  40614  poml4N  40617  osumcllem5N  40624  osumcllem7N  40626  pexmidlem2N  40635  pexmidlem4N  40637  pl42lem1N  40643  pl42lem2N  40644  pl42lem4N  40646  pl42N  40647  lhp2lt  40665  lhpexle2lem  40673  lhpexle3lem  40675  lhpj1  40686  lhpmcvr3  40689  lhpmcvr4N  40690  lhpmcvr5N  40691  lhpmcvr6N  40692  lhp2at0  40696  lhp2atnle  40697  lhpelim  40701  lhpmod2i2  40702  lhpmod6i1  40703  lhprelat3N  40704  lhple  40706  lhpat3  40710  4atexlemkl  40721  ltrnm  40795  ltrnj  40796  ltrnel  40803  ltrncnvel  40806  trljat1  40830  trljat2  40831  trlval3  40851  arglem1N  40854  cdlemc1  40855  cdlemc2  40856  cdlemc4  40858  cdlemc5  40859  cdlemc6  40860  cdlemd2  40863  cdlemd3  40864  cdlemd4  40865  cdlemd7  40868  cdleme0aa  40874  cdleme0b  40876  cdleme0c  40877  cdleme0e  40881  cdleme0fN  40882  cdlemeulpq  40884  cdleme01N  40885  cdleme0ex1N  40887  cdleme3g  40898  cdleme3h  40899  cdleme3  40901  cdleme4a  40903  cdleme5  40904  cdleme7aa  40906  cdleme7c  40909  cdleme7d  40910  cdleme7e  40911  cdleme7ga  40912  cdleme7  40913  cdleme8  40914  cdleme9  40917  cdleme10  40918  cdleme11c  40925  cdleme11e  40927  cdleme11fN  40928  cdleme11g  40929  cdleme11k  40932  cdleme11  40934  cdleme13  40936  cdleme15b  40939  cdleme15d  40941  cdleme15  40942  cdleme16b  40943  cdleme16e  40946  cdleme16f  40947  cdleme17b  40951  cdleme17c  40952  cdleme22gb  40958  cdlemednpq  40963  cdleme19b  40968  cdleme19c  40969  cdleme19e  40971  cdleme20aN  40973  cdleme20bN  40974  cdleme20c  40975  cdleme20d  40976  cdleme20e  40977  cdleme20j  40982  cdleme20k  40983  cdleme20l2  40985  cdleme20l  40986  cdleme20m  40987  cdleme21c  40991  cdleme21ct  40993  cdleme22aa  41003  cdleme22b  41005  cdleme22cN  41006  cdleme22d  41007  cdleme22e  41008  cdleme22eALTN  41009  cdleme22f  41010  cdleme22g  41012  cdleme23a  41013  cdleme23b  41014  cdleme23c  41015  cdleme27N  41033  cdleme28a  41034  cdleme28b  41035  cdleme29ex  41038  cdleme30a  41042  cdlemefr29exN  41066  cdleme32b  41106  cdleme32c  41107  cdleme32e  41109  cdleme35a  41112  cdleme35fnpq  41113  cdleme35b  41114  cdleme35c  41115  cdleme35d  41116  cdleme35f  41118  cdleme42c  41136  cdleme42e  41143  cdleme42h  41146  cdleme42i  41147  cdleme42mgN  41152  cdleme48bw  41166  cdlemeg46frv  41189  cdlemeg46vrg  41191  cdlemeg46rgv  41192  cdlemeg46req  41193  cdleme50eq  41205  cdlemf1  41225  trlord  41233  cdlemg2fv2  41264  cdlemg2m  41268  cdlemg7fvbwN  41271  cdlemg4c  41276  cdlemg4  41281  cdlemg6c  41284  cdlemg8b  41292  cdlemg10bALTN  41300  cdlemg10c  41303  cdlemg10  41305  cdlemg11b  41306  cdlemg12f  41312  cdlemg12g  41313  cdlemg12  41314  cdlemg13a  41315  cdlemg17a  41325  cdlemg17dALTN  41328  cdlemg17  41341  cdlemg18b  41343  cdlemg19a  41347  cdlemg19  41348  cdlemg27a  41356  cdlemg27b  41360  cdlemg31a  41361  cdlemg31b  41362  cdlemg33b0  41365  cdlemg33a  41370  cdlemg35  41377  trlcolem  41390  cdlemg42  41393  cdlemg44a  41395  cdlemg46  41399  trljco  41404  trljco2  41405  tendococl  41436  tendopltp  41444  cdlemh1  41479  cdlemh2  41480  cdlemi1  41482  cdlemi  41484  cdlemk3  41497  cdlemk4  41498  cdlemkvcl  41506  cdlemk10  41507  cdlemk7  41512  cdlemk11  41513  cdlemk12  41514  cdlemkole  41517  cdlemk14  41518  cdlemk15  41519  cdlemk1u  41523  cdlemk5u  41525  cdlemk7u  41534  cdlemk11u  41535  cdlemk12u  41536  cdlemk37  41578  cdlemk39  41580  cdlemkid1  41586  cdlemkid2  41588  cdlemk48  41614  cdlemk50  41616  cdlemk51  41617  cdlemk52  41618  cdlemk39u  41632  dia11N  41712  dia2dimlem1  41728  dia2dimlem2  41729  dia2dimlem3  41730  dia2dimlem10  41737  dia2dimlem12  41739  cdlemm10N  41782  dib11N  41824  diblss  41834  cdlemn2  41859  cdlemn10  41870  dihjustlem  41880  dihord1  41882  dihord2a  41883  dihord2b  41884  dihord2cN  41885  dihord11b  41886  dihord11c  41888  dihord2pre  41889  dihord2pre2  41890  dib2dim  41907  dih2dimb  41908  dihvalcq2  41911  dihopelvalcpre  41912  dihord6apre  41920  dihord5b  41923  dihord6b  41924  dihord5apre  41926  dih11  41929  dihwN  41953  dihmeetlem1N  41954  dihglblem5apreN  41955  dihglblem2N  41958  dihglblem3N  41959  dihmeetlem2N  41963  dihglbcpreN  41964  dihmeetbclemN  41968  dihmeetlem3N  41969  dihmeetlem4preN  41970  dihmeetlem6  41973  dihmeetlem7N  41974  dihjatc1  41975  dihjatc2N  41976  dihjatc3  41977  dihmeetlem9N  41979  dihmeetlem10N  41980  dihmeetlem11N  41981  dihmeetlem15N  41985  dihmeetlem16N  41986  dihmeetlem17N  41987  dihmeetlem19N  41989  dihmeetlem20N  41990  dihmeetALTN  41991  dihmeet2  42010  djhljjN  42066  djhj  42068  dihjatcclem1  42082  dihjatcclem2  42083  dihjatcclem4  42085  dihprrnlem1N  42088  dihprrnlem2  42089  dihjat6  42098  dihjat5N  42101  dvh4dimat  42102