Theorem hllatd 39988

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

Syntax hints:   → wi 4   ∈ wcel 2142  Latclat 18463  HLchlt 39974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-dm 5657  df-iota 6477  df-fv 6529  df-ov 7399  df-atl 39922  df-cvlat 39946  df-hlat 39975

This theorem is referenced by:  hlrelat  40026  hlrelat2  40027  exatleN  40028  intnatN  40031  hlrelat3  40036  cvrval3  40037  cvrexchlem  40043  lnnat  40051  2atlt  40063  atexchcvrN  40064  atbtwn  40070  4noncolr3  40077  athgt  40080  3dim0  40081  3dimlem3a  40084  3dimlem4a  40087  3dim3  40093  1cvratex  40097  1cvrjat  40099  hlatexch4  40105  ps-2b  40106  3atlem1  40107  3atlem2  40108  3atlem4  40110  3atlem5  40111  3atlem6  40112  2llnmat  40148  2at0mat0  40149  2atm  40151  ps-2c  40152  llnmlplnN  40163  lplnle  40164  2atmat  40185  lplnexllnN  40188  2llnjaN  40190  lvoli3  40201  lvoli2  40205  lvolnle3at  40206  islvol2aN  40216  4atlem3  40220  4atlem3a  40221  4atlem3b  40222  4atlem4a  40223  4atlem4b  40224  4atlem4c  40225  4atlem4d  40226  4atlem9  40227  4atlem10a  40228  4atlem10  40230  4atlem11a  40231  4atlem11b  40232  4atlem11  40233  4atlem12a  40234  4atlem12b  40235  4atlem12  40236  4at  40237  4at2  40238  lplncvrlvol2  40239  lplncvrlvol  40240  2lplnja  40243  dalemkelat  40248  lneq2at  40402  lncmp  40407  2lnat  40408  cdlema1N  40415  cdlemblem  40417  cdlemb  40418  paddasslem2  40445  paddasslem5  40448  paddasslem8  40451  paddasslem12  40455  paddasslem13  40456  paddasslem15  40458  pmodlem1  40470  pmodlem2  40471  atmod1i1m  40482  llnmod1i2  40484  llnmod2i2  40487  llnexchb2lem  40492  llnexchb2  40493  dalawlem1  40495  dalawlem2  40496  dalawlem3  40497  dalawlem4  40498  dalawlem5  40499  dalawlem6  40500  dalawlem7  40501  dalawlem8  40502  dalawlem9  40503  dalawlem11  40505  dalawlem12  40506  dalawlem15  40509  pclfinclN  40574  poml4N  40577  osumcllem5N  40584  osumcllem7N  40586  pexmidlem2N  40595  pexmidlem4N  40597  pl42lem1N  40603  pl42lem2N  40604  pl42lem4N  40606  pl42N  40607  lhp2lt  40625  lhpexle2lem  40633  lhpexle3lem  40635  lhpj1  40646  lhpmcvr3  40649  lhpmcvr4N  40650  lhpmcvr5N  40651  lhpmcvr6N  40652  lhp2at0  40656  lhp2atnle  40657  lhpelim  40661  lhpmod2i2  40662  lhpmod6i1  40663  lhprelat3N  40664  lhple  40666  lhpat3  40670  4atexlemkl  40681  ltrnm  40755  ltrnj  40756  ltrnel  40763  ltrncnvel  40766  trljat1  40790  trljat2  40791  trlval3  40811  arglem1N  40814  cdlemc1  40815  cdlemc2  40816  cdlemc4  40818  cdlemc5  40819  cdlemc6  40820  cdlemd2  40823  cdlemd3  40824  cdlemd4  40825  cdlemd7  40828  cdleme0aa  40834  cdleme0b  40836  cdleme0c  40837  cdleme0e  40841  cdleme0fN  40842  cdlemeulpq  40844  cdleme01N  40845  cdleme0ex1N  40847  cdleme3g  40858  cdleme3h  40859  cdleme3  40861  cdleme4a  40863  cdleme5  40864  cdleme7aa  40866  cdleme7c  40869  cdleme7d  40870  cdleme7e  40871  cdleme7ga  40872  cdleme7  40873  cdleme8  40874  cdleme9  40877  cdleme10  40878  cdleme11c  40885  cdleme11e  40887  cdleme11fN  40888  cdleme11g  40889  cdleme11k  40892  cdleme11  40894  cdleme13  40896  cdleme15b  40899  cdleme15d  40901  cdleme15  40902  cdleme16b  40903  cdleme16e  40906  cdleme16f  40907  cdleme17b  40911  cdleme17c  40912  cdleme22gb  40918  cdlemednpq  40923  cdleme19b  40928  cdleme19c  40929  cdleme19e  40931  cdleme20aN  40933  cdleme20bN  40934  cdleme20c  40935  cdleme20d  40936  cdleme20e  40937  cdleme20j  40942  cdleme20k  40943  cdleme20l2  40945  cdleme20l  40946  cdleme20m  40947  cdleme21c  40951  cdleme21ct  40953  cdleme22aa  40963  cdleme22b  40965  cdleme22cN  40966  cdleme22d  40967  cdleme22e  40968  cdleme22eALTN  40969  cdleme22f  40970  cdleme22g  40972  cdleme23a  40973  cdleme23b  40974  cdleme23c  40975  cdleme27N  40993  cdleme28a  40994  cdleme28b  40995  cdleme29ex  40998  cdleme30a  41002  cdlemefr29exN  41026  cdleme32b  41066  cdleme32c  41067  cdleme32e  41069  cdleme35a  41072  cdleme35fnpq  41073  cdleme35b  41074  cdleme35c  41075  cdleme35d  41076  cdleme35f  41078  cdleme42c  41096  cdleme42e  41103  cdleme42h  41106  cdleme42i  41107  cdleme42mgN  41112  cdleme48bw  41126  cdlemeg46frv  41149  cdlemeg46vrg  41151  cdlemeg46rgv  41152  cdlemeg46req  41153  cdleme50eq  41165  cdlemf1  41185  trlord  41193  cdlemg2fv2  41224  cdlemg2m  41228  cdlemg7fvbwN  41231  cdlemg4c  41236  cdlemg4  41241  cdlemg6c  41244  cdlemg8b  41252  cdlemg10bALTN  41260  cdlemg10c  41263  cdlemg10  41265  cdlemg11b  41266  cdlemg12f  41272  cdlemg12g  41273  cdlemg12  41274  cdlemg13a  41275  cdlemg17a  41285  cdlemg17dALTN  41288  cdlemg17  41301  cdlemg18b  41303  cdlemg19a  41307  cdlemg19  41308  cdlemg27a  41316  cdlemg27b  41320  cdlemg31a  41321  cdlemg31b  41322  cdlemg33b0  41325  cdlemg33a  41330  cdlemg35  41337  trlcolem  41350  cdlemg42  41353  cdlemg44a  41355  cdlemg46  41359  trljco  41364  trljco2  41365  tendococl  41396  tendopltp  41404  cdlemh1  41439  cdlemh2  41440  cdlemi1  41442  cdlemi  41444  cdlemk3  41457  cdlemk4  41458  cdlemkvcl  41466  cdlemk10  41467  cdlemk7  41472  cdlemk11  41473  cdlemk12  41474  cdlemkole  41477  cdlemk14  41478  cdlemk15  41479  cdlemk1u  41483  cdlemk5u  41485  cdlemk7u  41494  cdlemk11u  41495  cdlemk12u  41496  cdlemk37  41538  cdlemk39  41540  cdlemkid1  41546  cdlemkid2  41548  cdlemk48  41574  cdlemk50  41576  cdlemk51  41577  cdlemk52  41578  cdlemk39u  41592  dia11N  41672  dia2dimlem1  41688  dia2dimlem2  41689  dia2dimlem3  41690  dia2dimlem10  41697  dia2dimlem12  41699  cdlemm10N  41742  dib11N  41784  diblss  41794  cdlemn2  41819  cdlemn10  41830  dihjustlem  41840  dihord1  41842  dihord2a  41843  dihord2b  41844  dihord2cN  41845  dihord11b  41846  dihord11c  41848  dihord2pre  41849  dihord2pre2  41850  dib2dim  41867  dih2dimb  41868  dihvalcq2  41871  dihopelvalcpre  41872  dihord6apre  41880  dihord5b  41883  dihord6b  41884  dihord5apre  41886  dih11  41889  dihwN  41913  dihmeetlem1N  41914  dihglblem5apreN  41915  dihglblem2N  41918  dihglblem3N  41919  dihmeetlem2N  41923  dihglbcpreN  41924  dihmeetbclemN  41928  dihmeetlem3N  41929  dihmeetlem4preN  41930  dihmeetlem6  41933  dihmeetlem7N  41934  dihjatc1  41935  dihjatc2N  41936  dihjatc3  41937  dihmeetlem9N  41939  dihmeetlem10N  41940  dihmeetlem11N  41941  dihmeetlem15N  41945  dihmeetlem16N  41946  dihmeetlem17N  41947  dihmeetlem19N  41949  dihmeetlem20N  41950  dihmeetALTN  41951  dihmeet2  41970  djhljjN  42026  djhj  42028  dihjatcclem1  42042  dihjatcclem2  42043  dihjatcclem4  42045  dihprrnlem1N  42048  dihprrnlem2  42049  dihjat6  42058  dihjat5N  42061  dvh4dimat  42062