Theorem hllatd 39740

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

Syntax hints:   → wi 4   ∈ wcel 2114  Latclat 18366  HLchlt 39726

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-dm 5642  df-iota 6456  df-fv 6508  df-ov 7371  df-atl 39674  df-cvlat 39698  df-hlat 39727

This theorem is referenced by:  hlrelat  39778  hlrelat2  39779  exatleN  39780  intnatN  39783  hlrelat3  39788  cvrval3  39789  cvrexchlem  39795  lnnat  39803  2atlt  39815  atexchcvrN  39816  atbtwn  39822  4noncolr3  39829  athgt  39832  3dim0  39833  3dimlem3a  39836  3dimlem4a  39839  3dim3  39845  1cvratex  39849  1cvrjat  39851  hlatexch4  39857  ps-2b  39858  3atlem1  39859  3atlem2  39860  3atlem4  39862  3atlem5  39863  3atlem6  39864  2llnmat  39900  2at0mat0  39901  2atm  39903  ps-2c  39904  llnmlplnN  39915  lplnle  39916  2atmat  39937  lplnexllnN  39940  2llnjaN  39942  lvoli3  39953  lvoli2  39957  lvolnle3at  39958  islvol2aN  39968  4atlem3  39972  4atlem3a  39973  4atlem3b  39974  4atlem4a  39975  4atlem4b  39976  4atlem4c  39977  4atlem4d  39978  4atlem9  39979  4atlem10a  39980  4atlem10  39982  4atlem11a  39983  4atlem11b  39984  4atlem11  39985  4atlem12a  39986  4atlem12b  39987  4atlem12  39988  4at  39989  4at2  39990  lplncvrlvol2  39991  lplncvrlvol  39992  2lplnja  39995  dalemkelat  40000  lneq2at  40154  lncmp  40159  2lnat  40160  cdlema1N  40167  cdlemblem  40169  cdlemb  40170  paddasslem2  40197  paddasslem5  40200  paddasslem8  40203  paddasslem12  40207  paddasslem13  40208  paddasslem15  40210  pmodlem1  40222  pmodlem2  40223  atmod1i1m  40234  llnmod1i2  40236  llnmod2i2  40239  llnexchb2lem  40244  llnexchb2  40245  dalawlem1  40247  dalawlem2  40248  dalawlem3  40249  dalawlem4  40250  dalawlem5  40251  dalawlem6  40252  dalawlem7  40253  dalawlem8  40254  dalawlem9  40255  dalawlem11  40257  dalawlem12  40258  dalawlem15  40261  pclfinclN  40326  poml4N  40329  osumcllem5N  40336  osumcllem7N  40338  pexmidlem2N  40347  pexmidlem4N  40349  pl42lem1N  40355  pl42lem2N  40356  pl42lem4N  40358  pl42N  40359  lhp2lt  40377  lhpexle2lem  40385  lhpexle3lem  40387  lhpj1  40398  lhpmcvr3  40401  lhpmcvr4N  40402  lhpmcvr5N  40403  lhpmcvr6N  40404  lhp2at0  40408  lhp2atnle  40409  lhpelim  40413  lhpmod2i2  40414  lhpmod6i1  40415  lhprelat3N  40416  lhple  40418  lhpat3  40422  4atexlemkl  40433  ltrnm  40507  ltrnj  40508  ltrnel  40515  ltrncnvel  40518  trljat1  40542  trljat2  40543  trlval3  40563  arglem1N  40566  cdlemc1  40567  cdlemc2  40568  cdlemc4  40570  cdlemc5  40571  cdlemc6  40572  cdlemd2  40575  cdlemd3  40576  cdlemd4  40577  cdlemd7  40580  cdleme0aa  40586  cdleme0b  40588  cdleme0c  40589  cdleme0e  40593  cdleme0fN  40594  cdlemeulpq  40596  cdleme01N  40597  cdleme0ex1N  40599  cdleme3g  40610  cdleme3h  40611  cdleme3  40613  cdleme4a  40615  cdleme5  40616  cdleme7aa  40618  cdleme7c  40621  cdleme7d  40622  cdleme7e  40623  cdleme7ga  40624  cdleme7  40625  cdleme8  40626  cdleme9  40629  cdleme10  40630  cdleme11c  40637  cdleme11e  40639  cdleme11fN  40640  cdleme11g  40641  cdleme11k  40644  cdleme11  40646  cdleme13  40648  cdleme15b  40651  cdleme15d  40653  cdleme15  40654  cdleme16b  40655  cdleme16e  40658  cdleme16f  40659  cdleme17b  40663  cdleme17c  40664  cdleme22gb  40670  cdlemednpq  40675  cdleme19b  40680  cdleme19c  40681  cdleme19e  40683  cdleme20aN  40685  cdleme20bN  40686  cdleme20c  40687  cdleme20d  40688  cdleme20e  40689  cdleme20j  40694  cdleme20k  40695  cdleme20l2  40697  cdleme20l  40698  cdleme20m  40699  cdleme21c  40703  cdleme21ct  40705  cdleme22aa  40715  cdleme22b  40717  cdleme22cN  40718  cdleme22d  40719  cdleme22e  40720  cdleme22eALTN  40721  cdleme22f  40722  cdleme22g  40724  cdleme23a  40725  cdleme23b  40726  cdleme23c  40727  cdleme27N  40745  cdleme28a  40746  cdleme28b  40747  cdleme29ex  40750  cdleme30a  40754  cdlemefr29exN  40778  cdleme32b  40818  cdleme32c  40819  cdleme32e  40821  cdleme35a  40824  cdleme35fnpq  40825  cdleme35b  40826  cdleme35c  40827  cdleme35d  40828  cdleme35f  40830  cdleme42c  40848  cdleme42e  40855  cdleme42h  40858  cdleme42i  40859  cdleme42mgN  40864  cdleme48bw  40878  cdlemeg46frv  40901  cdlemeg46vrg  40903  cdlemeg46rgv  40904  cdlemeg46req  40905  cdleme50eq  40917  cdlemf1  40937  trlord  40945  cdlemg2fv2  40976  cdlemg2m  40980  cdlemg7fvbwN  40983  cdlemg4c  40988  cdlemg4  40993  cdlemg6c  40996  cdlemg8b  41004  cdlemg10bALTN  41012  cdlemg10c  41015  cdlemg10  41017  cdlemg11b  41018  cdlemg12f  41024  cdlemg12g  41025  cdlemg12  41026  cdlemg13a  41027  cdlemg17a  41037  cdlemg17dALTN  41040  cdlemg17  41053  cdlemg18b  41055  cdlemg19a  41059  cdlemg19  41060  cdlemg27a  41068  cdlemg27b  41072  cdlemg31a  41073  cdlemg31b  41074  cdlemg33b0  41077  cdlemg33a  41082  cdlemg35  41089  trlcolem  41102  cdlemg42  41105  cdlemg44a  41107  cdlemg46  41111  trljco  41116  trljco2  41117  tendococl  41148  tendopltp  41156  cdlemh1  41191  cdlemh2  41192  cdlemi1  41194  cdlemi  41196  cdlemk3  41209  cdlemk4  41210  cdlemkvcl  41218  cdlemk10  41219  cdlemk7  41224  cdlemk11  41225  cdlemk12  41226  cdlemkole  41229  cdlemk14  41230  cdlemk15  41231  cdlemk1u  41235  cdlemk5u  41237  cdlemk7u  41246  cdlemk11u  41247  cdlemk12u  41248  cdlemk37  41290  cdlemk39  41292  cdlemkid1  41298  cdlemkid2  41300  cdlemk48  41326  cdlemk50  41328  cdlemk51  41329  cdlemk52  41330  cdlemk39u  41344  dia11N  41424  dia2dimlem1  41440  dia2dimlem2  41441  dia2dimlem3  41442  dia2dimlem10  41449  dia2dimlem12  41451  cdlemm10N  41494  dib11N  41536  diblss  41546  cdlemn2  41571  cdlemn10  41582  dihjustlem  41592  dihord1  41594  dihord2a  41595  dihord2b  41596  dihord2cN  41597  dihord11b  41598  dihord11c  41600  dihord2pre  41601  dihord2pre2  41602  dib2dim  41619  dih2dimb  41620  dihvalcq2  41623  dihopelvalcpre  41624  dihord6apre  41632  dihord5b  41635  dihord6b  41636  dihord5apre  41638  dih11  41641  dihwN  41665  dihmeetlem1N  41666  dihglblem5apreN  41667  dihglblem2N  41670  dihglblem3N  41671  dihmeetlem2N  41675  dihglbcpreN  41676  dihmeetbclemN  41680  dihmeetlem3N  41681  dihmeetlem4preN  41682  dihmeetlem6  41685  dihmeetlem7N  41686  dihjatc1  41687  dihjatc2N  41688  dihjatc3  41689  dihmeetlem9N  41691  dihmeetlem10N  41692  dihmeetlem11N  41693  dihmeetlem15N  41697  dihmeetlem16N  41698  dihmeetlem17N  41699  dihmeetlem19N  41701  dihmeetlem20N  41702  dihmeetALTN  41703  dihmeet2  41722  djhljjN  41778  djhj  41780  dihjatcclem1  41794  dihjatcclem2  41795  dihjatcclem4  41797  dihprrnlem1N  41800  dihprrnlem2  41801  dihjat6  41810  dihjat5N  41813  dvh4dimat  41814