Theorem hllatd 36515

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

Syntax hints:   → wi 4   ∈ wcel 2114  Latclat 17655  HLchlt 36501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-dm 5565  df-iota 6314  df-fv 6363  df-ov 7159  df-atl 36449  df-cvlat 36473  df-hlat 36502

This theorem is referenced by:  hlrelat  36553  hlrelat2  36554  exatleN  36555  intnatN  36558  hlrelat3  36563  cvrval3  36564  cvrexchlem  36570  lnnat  36578  2atlt  36590  atexchcvrN  36591  atbtwn  36597  4noncolr3  36604  athgt  36607  3dim0  36608  3dimlem3a  36611  3dimlem4a  36614  3dim3  36620  1cvratex  36624  1cvrjat  36626  hlatexch4  36632  ps-2b  36633  3atlem1  36634  3atlem2  36635  3atlem4  36637  3atlem5  36638  3atlem6  36639  2llnmat  36675  2at0mat0  36676  2atm  36678  ps-2c  36679  llnmlplnN  36690  lplnle  36691  2atmat  36712  lplnexllnN  36715  2llnjaN  36717  lvoli3  36728  lvoli2  36732  lvolnle3at  36733  islvol2aN  36743  4atlem3  36747  4atlem3a  36748  4atlem3b  36749  4atlem4a  36750  4atlem4b  36751  4atlem4c  36752  4atlem4d  36753  4atlem9  36754  4atlem10a  36755  4atlem10  36757  4atlem11a  36758  4atlem11b  36759  4atlem11  36760  4atlem12a  36761  4atlem12b  36762  4atlem12  36763  4at  36764  4at2  36765  lplncvrlvol2  36766  lplncvrlvol  36767  2lplnja  36770  dalemkelat  36775  lneq2at  36929  lncmp  36934  2lnat  36935  cdlema1N  36942  cdlemblem  36944  cdlemb  36945  paddasslem2  36972  paddasslem5  36975  paddasslem8  36978  paddasslem12  36982  paddasslem13  36983  paddasslem15  36985  pmodlem1  36997  pmodlem2  36998  atmod1i1m  37009  llnmod1i2  37011  llnmod2i2  37014  llnexchb2lem  37019  llnexchb2  37020  dalawlem1  37022  dalawlem2  37023  dalawlem3  37024  dalawlem4  37025  dalawlem5  37026  dalawlem6  37027  dalawlem7  37028  dalawlem8  37029  dalawlem9  37030  dalawlem11  37032  dalawlem12  37033  dalawlem15  37036  pclfinclN  37101  poml4N  37104  osumcllem5N  37111  osumcllem7N  37113  pexmidlem2N  37122  pexmidlem4N  37124  pl42lem1N  37130  pl42lem2N  37131  pl42lem4N  37133  pl42N  37134  lhp2lt  37152  lhpexle2lem  37160  lhpexle3lem  37162  lhpj1  37173  lhpmcvr3  37176  lhpmcvr4N  37177  lhpmcvr5N  37178  lhpmcvr6N  37179  lhp2at0  37183  lhp2atnle  37184  lhpelim  37188  lhpmod2i2  37189  lhpmod6i1  37190  lhprelat3N  37191  lhple  37193  lhpat3  37197  4atexlemkl  37208  ltrnm  37282  ltrnj  37283  ltrnel  37290  ltrncnvel  37293  trljat1  37317  trljat2  37318  trlval3  37338  arglem1N  37341  cdlemc1  37342  cdlemc2  37343  cdlemc4  37345  cdlemc5  37346  cdlemc6  37347  cdlemd2  37350  cdlemd3  37351  cdlemd4  37352  cdlemd7  37355  cdleme0aa  37361  cdleme0b  37363  cdleme0c  37364  cdleme0e  37368  cdleme0fN  37369  cdlemeulpq  37371  cdleme01N  37372  cdleme0ex1N  37374  cdleme3g  37385  cdleme3h  37386  cdleme3  37388  cdleme4a  37390  cdleme5  37391  cdleme7aa  37393  cdleme7c  37396  cdleme7d  37397  cdleme7e  37398  cdleme7ga  37399  cdleme7  37400  cdleme8  37401  cdleme9  37404  cdleme10  37405  cdleme11c  37412  cdleme11e  37414  cdleme11fN  37415  cdleme11g  37416  cdleme11k  37419  cdleme11  37421  cdleme13  37423  cdleme15b  37426  cdleme15d  37428  cdleme15  37429  cdleme16b  37430  cdleme16e  37433  cdleme16f  37434  cdleme17b  37438  cdleme17c  37439  cdleme22gb  37445  cdlemednpq  37450  cdleme19b  37455  cdleme19c  37456  cdleme19e  37458  cdleme20aN  37460  cdleme20bN  37461  cdleme20c  37462  cdleme20d  37463  cdleme20e  37464  cdleme20j  37469  cdleme20k  37470  cdleme20l2  37472  cdleme20l  37473  cdleme20m  37474  cdleme21c  37478  cdleme21ct  37480  cdleme22aa  37490  cdleme22b  37492  cdleme22cN  37493  cdleme22d  37494  cdleme22e  37495  cdleme22eALTN  37496  cdleme22f  37497  cdleme22g  37499  cdleme23a  37500  cdleme23b  37501  cdleme23c  37502  cdleme27N  37520  cdleme28a  37521  cdleme28b  37522  cdleme29ex  37525  cdleme30a  37529  cdlemefr29exN  37553  cdleme32b  37593  cdleme32c  37594  cdleme32e  37596  cdleme35a  37599  cdleme35fnpq  37600  cdleme35b  37601  cdleme35c  37602  cdleme35d  37603  cdleme35f  37605  cdleme42c  37623  cdleme42e  37630  cdleme42h  37633  cdleme42i  37634  cdleme42mgN  37639  cdleme48bw  37653  cdlemeg46frv  37676  cdlemeg46vrg  37678  cdlemeg46rgv  37679  cdlemeg46req  37680  cdleme50eq  37692  cdlemf1  37712  trlord  37720  cdlemg2fv2  37751  cdlemg2m  37755  cdlemg7fvbwN  37758  cdlemg4c  37763  cdlemg4  37768  cdlemg6c  37771  cdlemg8b  37779  cdlemg10bALTN  37787  cdlemg10c  37790  cdlemg10  37792  cdlemg11b  37793  cdlemg12f  37799  cdlemg12g  37800  cdlemg12  37801  cdlemg13a  37802  cdlemg17a  37812  cdlemg17dALTN  37815  cdlemg17  37828  cdlemg18b  37830  cdlemg19a  37834  cdlemg19  37835  cdlemg27a  37843  cdlemg27b  37847  cdlemg31a  37848  cdlemg31b  37849  cdlemg33b0  37852  cdlemg33a  37857  cdlemg35  37864  trlcolem  37877  cdlemg42  37880  cdlemg44a  37882  cdlemg46  37886  trljco  37891  trljco2  37892  tendococl  37923  tendopltp  37931  cdlemh1  37966  cdlemh2  37967  cdlemi1  37969  cdlemi  37971  cdlemk3  37984  cdlemk4  37985  cdlemkvcl  37993  cdlemk10  37994  cdlemk7  37999  cdlemk11  38000  cdlemk12  38001  cdlemkole  38004  cdlemk14  38005  cdlemk15  38006  cdlemk1u  38010  cdlemk5u  38012  cdlemk7u  38021  cdlemk11u  38022  cdlemk12u  38023  cdlemk37  38065  cdlemk39  38067  cdlemkid1  38073  cdlemkid2  38075  cdlemk48  38101  cdlemk50  38103  cdlemk51  38104  cdlemk52  38105  cdlemk39u  38119  dia11N  38199  dia2dimlem1  38215  dia2dimlem2  38216  dia2dimlem3  38217  dia2dimlem10  38224  dia2dimlem12  38226  cdlemm10N  38269  dib11N  38311  diblss  38321  cdlemn2  38346  cdlemn10  38357  dihjustlem  38367  dihord1  38369  dihord2a  38370  dihord2b  38371  dihord2cN  38372  dihord11b  38373  dihord11c  38375  dihord2pre  38376  dihord2pre2  38377  dib2dim  38394  dih2dimb  38395  dihvalcq2  38398  dihopelvalcpre  38399  dihord6apre  38407  dihord5b  38410  dihord6b  38411  dihord5apre  38413  dih11  38416  dihwN  38440  dihmeetlem1N  38441  dihglblem5apreN  38442  dihglblem2N  38445  dihglblem3N  38446  dihmeetlem2N  38450  dihglbcpreN  38451  dihmeetbclemN  38455  dihmeetlem3N  38456  dihmeetlem4preN  38457  dihmeetlem6  38460  dihmeetlem7N  38461  dihjatc1  38462  dihjatc2N  38463  dihjatc3  38464  dihmeetlem9N  38466  dihmeetlem10N  38467  dihmeetlem11N  38468  dihmeetlem15N  38472  dihmeetlem16N  38473  dihmeetlem17N  38474  dihmeetlem19N  38476  dihmeetlem20N  38477  dihmeetALTN  38478  dihmeet2  38497  djhljjN  38553  djhj  38555  dihjatcclem1  38569  dihjatcclem2  38570  dihjatcclem4  38572  dihprrnlem1N  38575  dihprrnlem2  38576  dihjat6  38585  dihjat5N  38588  dvh4dimat  38589