Theorem hllatd 39365

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

Syntax hints:   → wi 4   ∈ wcel 2108  Latclat 18476  HLchlt 39351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-dm 5695  df-iota 6514  df-fv 6569  df-ov 7434  df-atl 39299  df-cvlat 39323  df-hlat 39352

This theorem is referenced by:  hlrelat  39404  hlrelat2  39405  exatleN  39406  intnatN  39409  hlrelat3  39414  cvrval3  39415  cvrexchlem  39421  lnnat  39429  2atlt  39441  atexchcvrN  39442  atbtwn  39448  4noncolr3  39455  athgt  39458  3dim0  39459  3dimlem3a  39462  3dimlem4a  39465  3dim3  39471  1cvratex  39475  1cvrjat  39477  hlatexch4  39483  ps-2b  39484  3atlem1  39485  3atlem2  39486  3atlem4  39488  3atlem5  39489  3atlem6  39490  2llnmat  39526  2at0mat0  39527  2atm  39529  ps-2c  39530  llnmlplnN  39541  lplnle  39542  2atmat  39563  lplnexllnN  39566  2llnjaN  39568  lvoli3  39579  lvoli2  39583  lvolnle3at  39584  islvol2aN  39594  4atlem3  39598  4atlem3a  39599  4atlem3b  39600  4atlem4a  39601  4atlem4b  39602  4atlem4c  39603  4atlem4d  39604  4atlem9  39605  4atlem10a  39606  4atlem10  39608  4atlem11a  39609  4atlem11b  39610  4atlem11  39611  4atlem12a  39612  4atlem12b  39613  4atlem12  39614  4at  39615  4at2  39616  lplncvrlvol2  39617  lplncvrlvol  39618  2lplnja  39621  dalemkelat  39626  lneq2at  39780  lncmp  39785  2lnat  39786  cdlema1N  39793  cdlemblem  39795  cdlemb  39796  paddasslem2  39823  paddasslem5  39826  paddasslem8  39829  paddasslem12  39833  paddasslem13  39834  paddasslem15  39836  pmodlem1  39848  pmodlem2  39849  atmod1i1m  39860  llnmod1i2  39862  llnmod2i2  39865  llnexchb2lem  39870  llnexchb2  39871  dalawlem1  39873  dalawlem2  39874  dalawlem3  39875  dalawlem4  39876  dalawlem5  39877  dalawlem6  39878  dalawlem7  39879  dalawlem8  39880  dalawlem9  39881  dalawlem11  39883  dalawlem12  39884  dalawlem15  39887  pclfinclN  39952  poml4N  39955  osumcllem5N  39962  osumcllem7N  39964  pexmidlem2N  39973  pexmidlem4N  39975  pl42lem1N  39981  pl42lem2N  39982  pl42lem4N  39984  pl42N  39985  lhp2lt  40003  lhpexle2lem  40011  lhpexle3lem  40013  lhpj1  40024  lhpmcvr3  40027  lhpmcvr4N  40028  lhpmcvr5N  40029  lhpmcvr6N  40030  lhp2at0  40034  lhp2atnle  40035  lhpelim  40039  lhpmod2i2  40040  lhpmod6i1  40041  lhprelat3N  40042  lhple  40044  lhpat3  40048  4atexlemkl  40059  ltrnm  40133  ltrnj  40134  ltrnel  40141  ltrncnvel  40144  trljat1  40168  trljat2  40169  trlval3  40189  arglem1N  40192  cdlemc1  40193  cdlemc2  40194  cdlemc4  40196  cdlemc5  40197  cdlemc6  40198  cdlemd2  40201  cdlemd3  40202  cdlemd4  40203  cdlemd7  40206  cdleme0aa  40212  cdleme0b  40214  cdleme0c  40215  cdleme0e  40219  cdleme0fN  40220  cdlemeulpq  40222  cdleme01N  40223  cdleme0ex1N  40225  cdleme3g  40236  cdleme3h  40237  cdleme3  40239  cdleme4a  40241  cdleme5  40242  cdleme7aa  40244  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme7  40251  cdleme8  40252  cdleme9  40255  cdleme10  40256  cdleme11c  40263  cdleme11e  40265  cdleme11fN  40266  cdleme11g  40267  cdleme11k  40270  cdleme11  40272  cdleme13  40274  cdleme15b  40277  cdleme15d  40279  cdleme15  40280  cdleme16b  40281  cdleme16e  40284  cdleme16f  40285  cdleme17b  40289  cdleme17c  40290  cdleme22gb  40296  cdlemednpq  40301  cdleme19b  40306  cdleme19c  40307  cdleme19e  40309  cdleme20aN  40311  cdleme20bN  40312  cdleme20c  40313  cdleme20d  40314  cdleme20e  40315  cdleme20j  40320  cdleme20k  40321  cdleme20l2  40323  cdleme20l  40324  cdleme20m  40325  cdleme21c  40329  cdleme21ct  40331  cdleme22aa  40341  cdleme22b  40343  cdleme22cN  40344  cdleme22d  40345  cdleme22e  40346  cdleme22eALTN  40347  cdleme22f  40348  cdleme22g  40350  cdleme23a  40351  cdleme23b  40352  cdleme23c  40353  cdleme27N  40371  cdleme28a  40372  cdleme28b  40373  cdleme29ex  40376  cdleme30a  40380  cdlemefr29exN  40404  cdleme32b  40444  cdleme32c  40445  cdleme32e  40447  cdleme35a  40450  cdleme35fnpq  40451  cdleme35b  40452  cdleme35c  40453  cdleme35d  40454  cdleme35f  40456  cdleme42c  40474  cdleme42e  40481  cdleme42h  40484  cdleme42i  40485  cdleme42mgN  40490  cdleme48bw  40504  cdlemeg46frv  40527  cdlemeg46vrg  40529  cdlemeg46rgv  40530  cdlemeg46req  40531  cdleme50eq  40543  cdlemf1  40563  trlord  40571  cdlemg2fv2  40602  cdlemg2m  40606  cdlemg7fvbwN  40609  cdlemg4c  40614  cdlemg4  40619  cdlemg6c  40622  cdlemg8b  40630  cdlemg10bALTN  40638  cdlemg10c  40641  cdlemg10  40643  cdlemg11b  40644  cdlemg12f  40650  cdlemg12g  40651  cdlemg12  40652  cdlemg13a  40653  cdlemg17a  40663  cdlemg17dALTN  40666  cdlemg17  40679  cdlemg18b  40681  cdlemg19a  40685  cdlemg19  40686  cdlemg27a  40694  cdlemg27b  40698  cdlemg31a  40699  cdlemg31b  40700  cdlemg33b0  40703  cdlemg33a  40708  cdlemg35  40715  trlcolem  40728  cdlemg42  40731  cdlemg44a  40733  cdlemg46  40737  trljco  40742  trljco2  40743  tendococl  40774  tendopltp  40782  cdlemh1  40817  cdlemh2  40818  cdlemi1  40820  cdlemi  40822  cdlemk3  40835  cdlemk4  40836  cdlemkvcl  40844  cdlemk10  40845  cdlemk7  40850  cdlemk11  40851  cdlemk12  40852  cdlemkole  40855  cdlemk14  40856  cdlemk15  40857  cdlemk1u  40861  cdlemk5u  40863  cdlemk7u  40872  cdlemk11u  40873  cdlemk12u  40874  cdlemk37  40916  cdlemk39  40918  cdlemkid1  40924  cdlemkid2  40926  cdlemk48  40952  cdlemk50  40954  cdlemk51  40955  cdlemk52  40956  cdlemk39u  40970  dia11N  41050  dia2dimlem1  41066  dia2dimlem2  41067  dia2dimlem3  41068  dia2dimlem10  41075  dia2dimlem12  41077  cdlemm10N  41120  dib11N  41162  diblss  41172  cdlemn2  41197  cdlemn10  41208  dihjustlem  41218  dihord1  41220  dihord2a  41221  dihord2b  41222  dihord2cN  41223  dihord11b  41224  dihord11c  41226  dihord2pre  41227  dihord2pre2  41228  dib2dim  41245  dih2dimb  41246  dihvalcq2  41249  dihopelvalcpre  41250  dihord6apre  41258  dihord5b  41261  dihord6b  41262  dihord5apre  41264  dih11  41267  dihwN  41291  dihmeetlem1N  41292  dihglblem5apreN  41293  dihglblem2N  41296  dihglblem3N  41297  dihmeetlem2N  41301  dihglbcpreN  41302  dihmeetbclemN  41306  dihmeetlem3N  41307  dihmeetlem4preN  41308  dihmeetlem6  41311  dihmeetlem7N  41312  dihjatc1  41313  dihjatc2N  41314  dihjatc3  41315  dihmeetlem9N  41317  dihmeetlem10N  41318  dihmeetlem11N  41319  dihmeetlem15N  41323  dihmeetlem16N  41324  dihmeetlem17N  41325  dihmeetlem19N  41327  dihmeetlem20N  41328  dihmeetALTN  41329  dihmeet2  41348  djhljjN  41404  djhj  41406  dihjatcclem1  41420  dihjatcclem2  41421  dihjatcclem4  41423  dihprrnlem1N  41426  dihprrnlem2  41427  dihjat6  41436  dihjat5N  41439  dvh4dimat  41440