Theorem hllatd 38282

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

Syntax hints:   → wi 4   ∈ wcel 2107  Latclat 18384  HLchlt 38268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-dm 5687  df-iota 6496  df-fv 6552  df-ov 7412  df-atl 38216  df-cvlat 38240  df-hlat 38269

This theorem is referenced by:  hlrelat  38321  hlrelat2  38322  exatleN  38323  intnatN  38326  hlrelat3  38331  cvrval3  38332  cvrexchlem  38338  lnnat  38346  2atlt  38358  atexchcvrN  38359  atbtwn  38365  4noncolr3  38372  athgt  38375  3dim0  38376  3dimlem3a  38379  3dimlem4a  38382  3dim3  38388  1cvratex  38392  1cvrjat  38394  hlatexch4  38400  ps-2b  38401  3atlem1  38402  3atlem2  38403  3atlem4  38405  3atlem5  38406  3atlem6  38407  2llnmat  38443  2at0mat0  38444  2atm  38446  ps-2c  38447  llnmlplnN  38458  lplnle  38459  2atmat  38480  lplnexllnN  38483  2llnjaN  38485  lvoli3  38496  lvoli2  38500  lvolnle3at  38501  islvol2aN  38511  4atlem3  38515  4atlem3a  38516  4atlem3b  38517  4atlem4a  38518  4atlem4b  38519  4atlem4c  38520  4atlem4d  38521  4atlem9  38522  4atlem10a  38523  4atlem10  38525  4atlem11a  38526  4atlem11b  38527  4atlem11  38528  4atlem12a  38529  4atlem12b  38530  4atlem12  38531  4at  38532  4at2  38533  lplncvrlvol2  38534  lplncvrlvol  38535  2lplnja  38538  dalemkelat  38543  lneq2at  38697  lncmp  38702  2lnat  38703  cdlema1N  38710  cdlemblem  38712  cdlemb  38713  paddasslem2  38740  paddasslem5  38743  paddasslem8  38746  paddasslem12  38750  paddasslem13  38751  paddasslem15  38753  pmodlem1  38765  pmodlem2  38766  atmod1i1m  38777  llnmod1i2  38779  llnmod2i2  38782  llnexchb2lem  38787  llnexchb2  38788  dalawlem1  38790  dalawlem2  38791  dalawlem3  38792  dalawlem4  38793  dalawlem5  38794  dalawlem6  38795  dalawlem7  38796  dalawlem8  38797  dalawlem9  38798  dalawlem11  38800  dalawlem12  38801  dalawlem15  38804  pclfinclN  38869  poml4N  38872  osumcllem5N  38879  osumcllem7N  38881  pexmidlem2N  38890  pexmidlem4N  38892  pl42lem1N  38898  pl42lem2N  38899  pl42lem4N  38901  pl42N  38902  lhp2lt  38920  lhpexle2lem  38928  lhpexle3lem  38930  lhpj1  38941  lhpmcvr3  38944  lhpmcvr4N  38945  lhpmcvr5N  38946  lhpmcvr6N  38947  lhp2at0  38951  lhp2atnle  38952  lhpelim  38956  lhpmod2i2  38957  lhpmod6i1  38958  lhprelat3N  38959  lhple  38961  lhpat3  38965  4atexlemkl  38976  ltrnm  39050  ltrnj  39051  ltrnel  39058  ltrncnvel  39061  trljat1  39085  trljat2  39086  trlval3  39106  arglem1N  39109  cdlemc1  39110  cdlemc2  39111  cdlemc4  39113  cdlemc5  39114  cdlemc6  39115  cdlemd2  39118  cdlemd3  39119  cdlemd4  39120  cdlemd7  39123  cdleme0aa  39129  cdleme0b  39131  cdleme0c  39132  cdleme0e  39136  cdleme0fN  39137  cdlemeulpq  39139  cdleme01N  39140  cdleme0ex1N  39142  cdleme3g  39153  cdleme3h  39154  cdleme3  39156  cdleme4a  39158  cdleme5  39159  cdleme7aa  39161  cdleme7c  39164  cdleme7d  39165  cdleme7e  39166  cdleme7ga  39167  cdleme7  39168  cdleme8  39169  cdleme9  39172  cdleme10  39173  cdleme11c  39180  cdleme11e  39182  cdleme11fN  39183  cdleme11g  39184  cdleme11k  39187  cdleme11  39189  cdleme13  39191  cdleme15b  39194  cdleme15d  39196  cdleme15  39197  cdleme16b  39198  cdleme16e  39201  cdleme16f  39202  cdleme17b  39206  cdleme17c  39207  cdleme22gb  39213  cdlemednpq  39218  cdleme19b  39223  cdleme19c  39224  cdleme19e  39226  cdleme20aN  39228  cdleme20bN  39229  cdleme20c  39230  cdleme20d  39231  cdleme20e  39232  cdleme20j  39237  cdleme20k  39238  cdleme20l2  39240  cdleme20l  39241  cdleme20m  39242  cdleme21c  39246  cdleme21ct  39248  cdleme22aa  39258  cdleme22b  39260  cdleme22cN  39261  cdleme22d  39262  cdleme22e  39263  cdleme22eALTN  39264  cdleme22f  39265  cdleme22g  39267  cdleme23a  39268  cdleme23b  39269  cdleme23c  39270  cdleme27N  39288  cdleme28a  39289  cdleme28b  39290  cdleme29ex  39293  cdleme30a  39297  cdlemefr29exN  39321  cdleme32b  39361  cdleme32c  39362  cdleme32e  39364  cdleme35a  39367  cdleme35fnpq  39368  cdleme35b  39369  cdleme35c  39370  cdleme35d  39371  cdleme35f  39373  cdleme42c  39391  cdleme42e  39398  cdleme42h  39401  cdleme42i  39402  cdleme42mgN  39407  cdleme48bw  39421  cdlemeg46frv  39444  cdlemeg46vrg  39446  cdlemeg46rgv  39447  cdlemeg46req  39448  cdleme50eq  39460  cdlemf1  39480  trlord  39488  cdlemg2fv2  39519  cdlemg2m  39523  cdlemg7fvbwN  39526  cdlemg4c  39531  cdlemg4  39536  cdlemg6c  39539  cdlemg8b  39547  cdlemg10bALTN  39555  cdlemg10c  39558  cdlemg10  39560  cdlemg11b  39561  cdlemg12f  39567  cdlemg12g  39568  cdlemg12  39569  cdlemg13a  39570  cdlemg17a  39580  cdlemg17dALTN  39583  cdlemg17  39596  cdlemg18b  39598  cdlemg19a  39602  cdlemg19  39603  cdlemg27a  39611  cdlemg27b  39615  cdlemg31a  39616  cdlemg31b  39617  cdlemg33b0  39620  cdlemg33a  39625  cdlemg35  39632  trlcolem  39645  cdlemg42  39648  cdlemg44a  39650  cdlemg46  39654  trljco  39659  trljco2  39660  tendococl  39691  tendopltp  39699  cdlemh1  39734  cdlemh2  39735  cdlemi1  39737  cdlemi  39739  cdlemk3  39752  cdlemk4  39753  cdlemkvcl  39761  cdlemk10  39762  cdlemk7  39767  cdlemk11  39768  cdlemk12  39769  cdlemkole  39772  cdlemk14  39773  cdlemk15  39774  cdlemk1u  39778  cdlemk5u  39780  cdlemk7u  39789  cdlemk11u  39790  cdlemk12u  39791  cdlemk37  39833  cdlemk39  39835  cdlemkid1  39841  cdlemkid2  39843  cdlemk48  39869  cdlemk50  39871  cdlemk51  39872  cdlemk52  39873  cdlemk39u  39887  dia11N  39967  dia2dimlem1  39983  dia2dimlem2  39984  dia2dimlem3  39985  dia2dimlem10  39992  dia2dimlem12  39994  cdlemm10N  40037  dib11N  40079  diblss  40089  cdlemn2  40114  cdlemn10  40125  dihjustlem  40135  dihord1  40137  dihord2a  40138  dihord2b  40139  dihord2cN  40140  dihord11b  40141  dihord11c  40143  dihord2pre  40144  dihord2pre2  40145  dib2dim  40162  dih2dimb  40163  dihvalcq2  40166  dihopelvalcpre  40167  dihord6apre  40175  dihord5b  40178  dihord6b  40179  dihord5apre  40181  dih11  40184  dihwN  40208  dihmeetlem1N  40209  dihglblem5apreN  40210  dihglblem2N  40213  dihglblem3N  40214  dihmeetlem2N  40218  dihglbcpreN  40219  dihmeetbclemN  40223  dihmeetlem3N  40224  dihmeetlem4preN  40225  dihmeetlem6  40228  dihmeetlem7N  40229  dihjatc1  40230  dihjatc2N  40231  dihjatc3  40232  dihmeetlem9N  40234  dihmeetlem10N  40235  dihmeetlem11N  40236  dihmeetlem15N  40240  dihmeetlem16N  40241  dihmeetlem17N  40242  dihmeetlem19N  40244  dihmeetlem20N  40245  dihmeetALTN  40246  dihmeet2  40265  djhljjN  40321  djhj  40323  dihjatcclem1  40337  dihjatcclem2  40338  dihjatcclem4  40340  dihprrnlem1N  40343  dihprrnlem2  40344  dihjat6  40353  dihjat5N  40356  dvh4dimat  40357