Theorem hllatd 39810

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

Syntax hints:   → wi 4   ∈ wcel 2114  Latclat 18397  HLchlt 39796

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-dm 5641  df-iota 6454  df-fv 6506  df-ov 7370  df-atl 39744  df-cvlat 39768  df-hlat 39797

This theorem is referenced by:  hlrelat  39848  hlrelat2  39849  exatleN  39850  intnatN  39853  hlrelat3  39858  cvrval3  39859  cvrexchlem  39865  lnnat  39873  2atlt  39885  atexchcvrN  39886  atbtwn  39892  4noncolr3  39899  athgt  39902  3dim0  39903  3dimlem3a  39906  3dimlem4a  39909  3dim3  39915  1cvratex  39919  1cvrjat  39921  hlatexch4  39927  ps-2b  39928  3atlem1  39929  3atlem2  39930  3atlem4  39932  3atlem5  39933  3atlem6  39934  2llnmat  39970  2at0mat0  39971  2atm  39973  ps-2c  39974  llnmlplnN  39985  lplnle  39986  2atmat  40007  lplnexllnN  40010  2llnjaN  40012  lvoli3  40023  lvoli2  40027  lvolnle3at  40028  islvol2aN  40038  4atlem3  40042  4atlem3a  40043  4atlem3b  40044  4atlem4a  40045  4atlem4b  40046  4atlem4c  40047  4atlem4d  40048  4atlem9  40049  4atlem10a  40050  4atlem10  40052  4atlem11a  40053  4atlem11b  40054  4atlem11  40055  4atlem12a  40056  4atlem12b  40057  4atlem12  40058  4at  40059  4at2  40060  lplncvrlvol2  40061  lplncvrlvol  40062  2lplnja  40065  dalemkelat  40070  lneq2at  40224  lncmp  40229  2lnat  40230  cdlema1N  40237  cdlemblem  40239  cdlemb  40240  paddasslem2  40267  paddasslem5  40270  paddasslem8  40273  paddasslem12  40277  paddasslem13  40278  paddasslem15  40280  pmodlem1  40292  pmodlem2  40293  atmod1i1m  40304  llnmod1i2  40306  llnmod2i2  40309  llnexchb2lem  40314  llnexchb2  40315  dalawlem1  40317  dalawlem2  40318  dalawlem3  40319  dalawlem4  40320  dalawlem5  40321  dalawlem6  40322  dalawlem7  40323  dalawlem8  40324  dalawlem9  40325  dalawlem11  40327  dalawlem12  40328  dalawlem15  40331  pclfinclN  40396  poml4N  40399  osumcllem5N  40406  osumcllem7N  40408  pexmidlem2N  40417  pexmidlem4N  40419  pl42lem1N  40425  pl42lem2N  40426  pl42lem4N  40428  pl42N  40429  lhp2lt  40447  lhpexle2lem  40455  lhpexle3lem  40457  lhpj1  40468  lhpmcvr3  40471  lhpmcvr4N  40472  lhpmcvr5N  40473  lhpmcvr6N  40474  lhp2at0  40478  lhp2atnle  40479  lhpelim  40483  lhpmod2i2  40484  lhpmod6i1  40485  lhprelat3N  40486  lhple  40488  lhpat3  40492  4atexlemkl  40503  ltrnm  40577  ltrnj  40578  ltrnel  40585  ltrncnvel  40588  trljat1  40612  trljat2  40613  trlval3  40633  arglem1N  40636  cdlemc1  40637  cdlemc2  40638  cdlemc4  40640  cdlemc5  40641  cdlemc6  40642  cdlemd2  40645  cdlemd3  40646  cdlemd4  40647  cdlemd7  40650  cdleme0aa  40656  cdleme0b  40658  cdleme0c  40659  cdleme0e  40663  cdleme0fN  40664  cdlemeulpq  40666  cdleme01N  40667  cdleme0ex1N  40669  cdleme3g  40680  cdleme3h  40681  cdleme3  40683  cdleme4a  40685  cdleme5  40686  cdleme7aa  40688  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme8  40696  cdleme9  40699  cdleme10  40700  cdleme11c  40707  cdleme11e  40709  cdleme11fN  40710  cdleme11g  40711  cdleme11k  40714  cdleme11  40716  cdleme13  40718  cdleme15b  40721  cdleme15d  40723  cdleme15  40724  cdleme16b  40725  cdleme16e  40728  cdleme16f  40729  cdleme17b  40733  cdleme17c  40734  cdleme22gb  40740  cdlemednpq  40745  cdleme19b  40750  cdleme19c  40751  cdleme19e  40753  cdleme20aN  40755  cdleme20bN  40756  cdleme20c  40757  cdleme20d  40758  cdleme20e  40759  cdleme20j  40764  cdleme20k  40765  cdleme20l2  40767  cdleme20l  40768  cdleme20m  40769  cdleme21c  40773  cdleme21ct  40775  cdleme22aa  40785  cdleme22b  40787  cdleme22cN  40788  cdleme22d  40789  cdleme22e  40790  cdleme22eALTN  40791  cdleme22f  40792  cdleme22g  40794  cdleme23a  40795  cdleme23b  40796  cdleme23c  40797  cdleme27N  40815  cdleme28a  40816  cdleme28b  40817  cdleme29ex  40820  cdleme30a  40824  cdlemefr29exN  40848  cdleme32b  40888  cdleme32c  40889  cdleme32e  40891  cdleme35a  40894  cdleme35fnpq  40895  cdleme35b  40896  cdleme35c  40897  cdleme35d  40898  cdleme35f  40900  cdleme42c  40918  cdleme42e  40925  cdleme42h  40928  cdleme42i  40929  cdleme42mgN  40934  cdleme48bw  40948  cdlemeg46frv  40971  cdlemeg46vrg  40973  cdlemeg46rgv  40974  cdlemeg46req  40975  cdleme50eq  40987  cdlemf1  41007  trlord  41015  cdlemg2fv2  41046  cdlemg2m  41050  cdlemg7fvbwN  41053  cdlemg4c  41058  cdlemg4  41063  cdlemg6c  41066  cdlemg8b  41074  cdlemg10bALTN  41082  cdlemg10c  41085  cdlemg10  41087  cdlemg11b  41088  cdlemg12f  41094  cdlemg12g  41095  cdlemg12  41096  cdlemg13a  41097  cdlemg17a  41107  cdlemg17dALTN  41110  cdlemg17  41123  cdlemg18b  41125  cdlemg19a  41129  cdlemg19  41130  cdlemg27a  41138  cdlemg27b  41142  cdlemg31a  41143  cdlemg31b  41144  cdlemg33b0  41147  cdlemg33a  41152  cdlemg35  41159  trlcolem  41172  cdlemg42  41175  cdlemg44a  41177  cdlemg46  41181  trljco  41186  trljco2  41187  tendococl  41218  tendopltp  41226  cdlemh1  41261  cdlemh2  41262  cdlemi1  41264  cdlemi  41266  cdlemk3  41279  cdlemk4  41280  cdlemkvcl  41288  cdlemk10  41289  cdlemk7  41294  cdlemk11  41295  cdlemk12  41296  cdlemkole  41299  cdlemk14  41300  cdlemk15  41301  cdlemk1u  41305  cdlemk5u  41307  cdlemk7u  41316  cdlemk11u  41317  cdlemk12u  41318  cdlemk37  41360  cdlemk39  41362  cdlemkid1  41368  cdlemkid2  41370  cdlemk48  41396  cdlemk50  41398  cdlemk51  41399  cdlemk52  41400  cdlemk39u  41414  dia11N  41494  dia2dimlem1  41510  dia2dimlem2  41511  dia2dimlem3  41512  dia2dimlem10  41519  dia2dimlem12  41521  cdlemm10N  41564  dib11N  41606  diblss  41616  cdlemn2  41641  cdlemn10  41652  dihjustlem  41662  dihord1  41664  dihord2a  41665  dihord2b  41666  dihord2cN  41667  dihord11b  41668  dihord11c  41670  dihord2pre  41671  dihord2pre2  41672  dib2dim  41689  dih2dimb  41690  dihvalcq2  41693  dihopelvalcpre  41694  dihord6apre  41702  dihord5b  41705  dihord6b  41706  dihord5apre  41708  dih11  41711  dihwN  41735  dihmeetlem1N  41736  dihglblem5apreN  41737  dihglblem2N  41740  dihglblem3N  41741  dihmeetlem2N  41745  dihglbcpreN  41746  dihmeetbclemN  41750  dihmeetlem3N  41751  dihmeetlem4preN  41752  dihmeetlem6  41755  dihmeetlem7N  41756  dihjatc1  41757  dihjatc2N  41758  dihjatc3  41759  dihmeetlem9N  41761  dihmeetlem10N  41762  dihmeetlem11N  41763  dihmeetlem15N  41767  dihmeetlem16N  41768  dihmeetlem17N  41769  dihmeetlem19N  41771  dihmeetlem20N  41772  dihmeetALTN  41773  dihmeet2  41792  djhljjN  41848  djhj  41850  dihjatcclem1  41864  dihjatcclem2  41865  dihjatcclem4  41867  dihprrnlem1N  41870  dihprrnlem2  41871  dihjat6  41880  dihjat5N  41883  dvh4dimat  41884