Theorem hllatd 37305

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

Syntax hints:   → wi 4   ∈ wcel 2108  Latclat 18064  HLchlt 37291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-dm 5590  df-iota 6376  df-fv 6426  df-ov 7258  df-atl 37239  df-cvlat 37263  df-hlat 37292

This theorem is referenced by:  hlrelat  37343  hlrelat2  37344  exatleN  37345  intnatN  37348  hlrelat3  37353  cvrval3  37354  cvrexchlem  37360  lnnat  37368  2atlt  37380  atexchcvrN  37381  atbtwn  37387  4noncolr3  37394  athgt  37397  3dim0  37398  3dimlem3a  37401  3dimlem4a  37404  3dim3  37410  1cvratex  37414  1cvrjat  37416  hlatexch4  37422  ps-2b  37423  3atlem1  37424  3atlem2  37425  3atlem4  37427  3atlem5  37428  3atlem6  37429  2llnmat  37465  2at0mat0  37466  2atm  37468  ps-2c  37469  llnmlplnN  37480  lplnle  37481  2atmat  37502  lplnexllnN  37505  2llnjaN  37507  lvoli3  37518  lvoli2  37522  lvolnle3at  37523  islvol2aN  37533  4atlem3  37537  4atlem3a  37538  4atlem3b  37539  4atlem4a  37540  4atlem4b  37541  4atlem4c  37542  4atlem4d  37543  4atlem9  37544  4atlem10a  37545  4atlem10  37547  4atlem11a  37548  4atlem11b  37549  4atlem11  37550  4atlem12a  37551  4atlem12b  37552  4atlem12  37553  4at  37554  4at2  37555  lplncvrlvol2  37556  lplncvrlvol  37557  2lplnja  37560  dalemkelat  37565  lneq2at  37719  lncmp  37724  2lnat  37725  cdlema1N  37732  cdlemblem  37734  cdlemb  37735  paddasslem2  37762  paddasslem5  37765  paddasslem8  37768  paddasslem12  37772  paddasslem13  37773  paddasslem15  37775  pmodlem1  37787  pmodlem2  37788  atmod1i1m  37799  llnmod1i2  37801  llnmod2i2  37804  llnexchb2lem  37809  llnexchb2  37810  dalawlem1  37812  dalawlem2  37813  dalawlem3  37814  dalawlem4  37815  dalawlem5  37816  dalawlem6  37817  dalawlem7  37818  dalawlem8  37819  dalawlem9  37820  dalawlem11  37822  dalawlem12  37823  dalawlem15  37826  pclfinclN  37891  poml4N  37894  osumcllem5N  37901  osumcllem7N  37903  pexmidlem2N  37912  pexmidlem4N  37914  pl42lem1N  37920  pl42lem2N  37921  pl42lem4N  37923  pl42N  37924  lhp2lt  37942  lhpexle2lem  37950  lhpexle3lem  37952  lhpj1  37963  lhpmcvr3  37966  lhpmcvr4N  37967  lhpmcvr5N  37968  lhpmcvr6N  37969  lhp2at0  37973  lhp2atnle  37974  lhpelim  37978  lhpmod2i2  37979  lhpmod6i1  37980  lhprelat3N  37981  lhple  37983  lhpat3  37987  4atexlemkl  37998  ltrnm  38072  ltrnj  38073  ltrnel  38080  ltrncnvel  38083  trljat1  38107  trljat2  38108  trlval3  38128  arglem1N  38131  cdlemc1  38132  cdlemc2  38133  cdlemc4  38135  cdlemc5  38136  cdlemc6  38137  cdlemd2  38140  cdlemd3  38141  cdlemd4  38142  cdlemd7  38145  cdleme0aa  38151  cdleme0b  38153  cdleme0c  38154  cdleme0e  38158  cdleme0fN  38159  cdlemeulpq  38161  cdleme01N  38162  cdleme0ex1N  38164  cdleme3g  38175  cdleme3h  38176  cdleme3  38178  cdleme4a  38180  cdleme5  38181  cdleme7aa  38183  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme7  38190  cdleme8  38191  cdleme9  38194  cdleme10  38195  cdleme11c  38202  cdleme11e  38204  cdleme11fN  38205  cdleme11g  38206  cdleme11k  38209  cdleme11  38211  cdleme13  38213  cdleme15b  38216  cdleme15d  38218  cdleme15  38219  cdleme16b  38220  cdleme16e  38223  cdleme16f  38224  cdleme17b  38228  cdleme17c  38229  cdleme22gb  38235  cdlemednpq  38240  cdleme19b  38245  cdleme19c  38246  cdleme19e  38248  cdleme20aN  38250  cdleme20bN  38251  cdleme20c  38252  cdleme20d  38253  cdleme20e  38254  cdleme20j  38259  cdleme20k  38260  cdleme20l2  38262  cdleme20l  38263  cdleme20m  38264  cdleme21c  38268  cdleme21ct  38270  cdleme22aa  38280  cdleme22b  38282  cdleme22cN  38283  cdleme22d  38284  cdleme22e  38285  cdleme22eALTN  38286  cdleme22f  38287  cdleme22g  38289  cdleme23a  38290  cdleme23b  38291  cdleme23c  38292  cdleme27N  38310  cdleme28a  38311  cdleme28b  38312  cdleme29ex  38315  cdleme30a  38319  cdlemefr29exN  38343  cdleme32b  38383  cdleme32c  38384  cdleme32e  38386  cdleme35a  38389  cdleme35fnpq  38390  cdleme35b  38391  cdleme35c  38392  cdleme35d  38393  cdleme35f  38395  cdleme42c  38413  cdleme42e  38420  cdleme42h  38423  cdleme42i  38424  cdleme42mgN  38429  cdleme48bw  38443  cdlemeg46frv  38466  cdlemeg46vrg  38468  cdlemeg46rgv  38469  cdlemeg46req  38470  cdleme50eq  38482  cdlemf1  38502  trlord  38510  cdlemg2fv2  38541  cdlemg2m  38545  cdlemg7fvbwN  38548  cdlemg4c  38553  cdlemg4  38558  cdlemg6c  38561  cdlemg8b  38569  cdlemg10bALTN  38577  cdlemg10c  38580  cdlemg10  38582  cdlemg11b  38583  cdlemg12f  38589  cdlemg12g  38590  cdlemg12  38591  cdlemg13a  38592  cdlemg17a  38602  cdlemg17dALTN  38605  cdlemg17  38618  cdlemg18b  38620  cdlemg19a  38624  cdlemg19  38625  cdlemg27a  38633  cdlemg27b  38637  cdlemg31a  38638  cdlemg31b  38639  cdlemg33b0  38642  cdlemg33a  38647  cdlemg35  38654  trlcolem  38667  cdlemg42  38670  cdlemg44a  38672  cdlemg46  38676  trljco  38681  trljco2  38682  tendococl  38713  tendopltp  38721  cdlemh1  38756  cdlemh2  38757  cdlemi1  38759  cdlemi  38761  cdlemk3  38774  cdlemk4  38775  cdlemkvcl  38783  cdlemk10  38784  cdlemk7  38789  cdlemk11  38790  cdlemk12  38791  cdlemkole  38794  cdlemk14  38795  cdlemk15  38796  cdlemk1u  38800  cdlemk5u  38802  cdlemk7u  38811  cdlemk11u  38812  cdlemk12u  38813  cdlemk37  38855  cdlemk39  38857  cdlemkid1  38863  cdlemkid2  38865  cdlemk48  38891  cdlemk50  38893  cdlemk51  38894  cdlemk52  38895  cdlemk39u  38909  dia11N  38989  dia2dimlem1  39005  dia2dimlem2  39006  dia2dimlem3  39007  dia2dimlem10  39014  dia2dimlem12  39016  cdlemm10N  39059  dib11N  39101  diblss  39111  cdlemn2  39136  cdlemn10  39147  dihjustlem  39157  dihord1  39159  dihord2a  39160  dihord2b  39161  dihord2cN  39162  dihord11b  39163  dihord11c  39165  dihord2pre  39166  dihord2pre2  39167  dib2dim  39184  dih2dimb  39185  dihvalcq2  39188  dihopelvalcpre  39189  dihord6apre  39197  dihord5b  39200  dihord6b  39201  dihord5apre  39203  dih11  39206  dihwN  39230  dihmeetlem1N  39231  dihglblem5apreN  39232  dihglblem2N  39235  dihglblem3N  39236  dihmeetlem2N  39240  dihglbcpreN  39241  dihmeetbclemN  39245  dihmeetlem3N  39246  dihmeetlem4preN  39247  dihmeetlem6  39250  dihmeetlem7N  39251  dihjatc1  39252  dihjatc2N  39253  dihjatc3  39254  dihmeetlem9N  39256  dihmeetlem10N  39257  dihmeetlem11N  39258  dihmeetlem15N  39262  dihmeetlem16N  39263  dihmeetlem17N  39264  dihmeetlem19N  39266  dihmeetlem20N  39267  dihmeetALTN  39268  dihmeet2  39287  djhljjN  39343  djhj  39345  dihjatcclem1  39359  dihjatcclem2  39360  dihjatcclem4  39362  dihprrnlem1N  39365  dihprrnlem2  39366  dihjat6  39375  dihjat5N  39378  dvh4dimat  39379