Theorem hllatd 37385

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

Syntax hints:   → wi 4   ∈ wcel 2107  Latclat 18158  HLchlt 37371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-dm 5600  df-iota 6395  df-fv 6445  df-ov 7287  df-atl 37319  df-cvlat 37343  df-hlat 37372

This theorem is referenced by:  hlrelat  37423  hlrelat2  37424  exatleN  37425  intnatN  37428  hlrelat3  37433  cvrval3  37434  cvrexchlem  37440  lnnat  37448  2atlt  37460  atexchcvrN  37461  atbtwn  37467  4noncolr3  37474  athgt  37477  3dim0  37478  3dimlem3a  37481  3dimlem4a  37484  3dim3  37490  1cvratex  37494  1cvrjat  37496  hlatexch4  37502  ps-2b  37503  3atlem1  37504  3atlem2  37505  3atlem4  37507  3atlem5  37508  3atlem6  37509  2llnmat  37545  2at0mat0  37546  2atm  37548  ps-2c  37549  llnmlplnN  37560  lplnle  37561  2atmat  37582  lplnexllnN  37585  2llnjaN  37587  lvoli3  37598  lvoli2  37602  lvolnle3at  37603  islvol2aN  37613  4atlem3  37617  4atlem3a  37618  4atlem3b  37619  4atlem4a  37620  4atlem4b  37621  4atlem4c  37622  4atlem4d  37623  4atlem9  37624  4atlem10a  37625  4atlem10  37627  4atlem11a  37628  4atlem11b  37629  4atlem11  37630  4atlem12a  37631  4atlem12b  37632  4atlem12  37633  4at  37634  4at2  37635  lplncvrlvol2  37636  lplncvrlvol  37637  2lplnja  37640  dalemkelat  37645  lneq2at  37799  lncmp  37804  2lnat  37805  cdlema1N  37812  cdlemblem  37814  cdlemb  37815  paddasslem2  37842  paddasslem5  37845  paddasslem8  37848  paddasslem12  37852  paddasslem13  37853  paddasslem15  37855  pmodlem1  37867  pmodlem2  37868  atmod1i1m  37879  llnmod1i2  37881  llnmod2i2  37884  llnexchb2lem  37889  llnexchb2  37890  dalawlem1  37892  dalawlem2  37893  dalawlem3  37894  dalawlem4  37895  dalawlem5  37896  dalawlem6  37897  dalawlem7  37898  dalawlem8  37899  dalawlem9  37900  dalawlem11  37902  dalawlem12  37903  dalawlem15  37906  pclfinclN  37971  poml4N  37974  osumcllem5N  37981  osumcllem7N  37983  pexmidlem2N  37992  pexmidlem4N  37994  pl42lem1N  38000  pl42lem2N  38001  pl42lem4N  38003  pl42N  38004  lhp2lt  38022  lhpexle2lem  38030  lhpexle3lem  38032  lhpj1  38043  lhpmcvr3  38046  lhpmcvr4N  38047  lhpmcvr5N  38048  lhpmcvr6N  38049  lhp2at0  38053  lhp2atnle  38054  lhpelim  38058  lhpmod2i2  38059  lhpmod6i1  38060  lhprelat3N  38061  lhple  38063  lhpat3  38067  4atexlemkl  38078  ltrnm  38152  ltrnj  38153  ltrnel  38160  ltrncnvel  38163  trljat1  38187  trljat2  38188  trlval3  38208  arglem1N  38211  cdlemc1  38212  cdlemc2  38213  cdlemc4  38215  cdlemc5  38216  cdlemc6  38217  cdlemd2  38220  cdlemd3  38221  cdlemd4  38222  cdlemd7  38225  cdleme0aa  38231  cdleme0b  38233  cdleme0c  38234  cdleme0e  38238  cdleme0fN  38239  cdlemeulpq  38241  cdleme01N  38242  cdleme0ex1N  38244  cdleme3g  38255  cdleme3h  38256  cdleme3  38258  cdleme4a  38260  cdleme5  38261  cdleme7aa  38263  cdleme7c  38266  cdleme7d  38267  cdleme7e  38268  cdleme7ga  38269  cdleme7  38270  cdleme8  38271  cdleme9  38274  cdleme10  38275  cdleme11c  38282  cdleme11e  38284  cdleme11fN  38285  cdleme11g  38286  cdleme11k  38289  cdleme11  38291  cdleme13  38293  cdleme15b  38296  cdleme15d  38298  cdleme15  38299  cdleme16b  38300  cdleme16e  38303  cdleme16f  38304  cdleme17b  38308  cdleme17c  38309  cdleme22gb  38315  cdlemednpq  38320  cdleme19b  38325  cdleme19c  38326  cdleme19e  38328  cdleme20aN  38330  cdleme20bN  38331  cdleme20c  38332  cdleme20d  38333  cdleme20e  38334  cdleme20j  38339  cdleme20k  38340  cdleme20l2  38342  cdleme20l  38343  cdleme20m  38344  cdleme21c  38348  cdleme21ct  38350  cdleme22aa  38360  cdleme22b  38362  cdleme22cN  38363  cdleme22d  38364  cdleme22e  38365  cdleme22eALTN  38366  cdleme22f  38367  cdleme22g  38369  cdleme23a  38370  cdleme23b  38371  cdleme23c  38372  cdleme27N  38390  cdleme28a  38391  cdleme28b  38392  cdleme29ex  38395  cdleme30a  38399  cdlemefr29exN  38423  cdleme32b  38463  cdleme32c  38464  cdleme32e  38466  cdleme35a  38469  cdleme35fnpq  38470  cdleme35b  38471  cdleme35c  38472  cdleme35d  38473  cdleme35f  38475  cdleme42c  38493  cdleme42e  38500  cdleme42h  38503  cdleme42i  38504  cdleme42mgN  38509  cdleme48bw  38523  cdlemeg46frv  38546  cdlemeg46vrg  38548  cdlemeg46rgv  38549  cdlemeg46req  38550  cdleme50eq  38562  cdlemf1  38582  trlord  38590  cdlemg2fv2  38621  cdlemg2m  38625  cdlemg7fvbwN  38628  cdlemg4c  38633  cdlemg4  38638  cdlemg6c  38641  cdlemg8b  38649  cdlemg10bALTN  38657  cdlemg10c  38660  cdlemg10  38662  cdlemg11b  38663  cdlemg12f  38669  cdlemg12g  38670  cdlemg12  38671  cdlemg13a  38672  cdlemg17a  38682  cdlemg17dALTN  38685  cdlemg17  38698  cdlemg18b  38700  cdlemg19a  38704  cdlemg19  38705  cdlemg27a  38713  cdlemg27b  38717  cdlemg31a  38718  cdlemg31b  38719  cdlemg33b0  38722  cdlemg33a  38727  cdlemg35  38734  trlcolem  38747  cdlemg42  38750  cdlemg44a  38752  cdlemg46  38756  trljco  38761  trljco2  38762  tendococl  38793  tendopltp  38801  cdlemh1  38836  cdlemh2  38837  cdlemi1  38839  cdlemi  38841  cdlemk3  38854  cdlemk4  38855  cdlemkvcl  38863  cdlemk10  38864  cdlemk7  38869  cdlemk11  38870  cdlemk12  38871  cdlemkole  38874  cdlemk14  38875  cdlemk15  38876  cdlemk1u  38880  cdlemk5u  38882  cdlemk7u  38891  cdlemk11u  38892  cdlemk12u  38893  cdlemk37  38935  cdlemk39  38937  cdlemkid1  38943  cdlemkid2  38945  cdlemk48  38971  cdlemk50  38973  cdlemk51  38974  cdlemk52  38975  cdlemk39u  38989  dia11N  39069  dia2dimlem1  39085  dia2dimlem2  39086  dia2dimlem3  39087  dia2dimlem10  39094  dia2dimlem12  39096  cdlemm10N  39139  dib11N  39181  diblss  39191  cdlemn2  39216  cdlemn10  39227  dihjustlem  39237  dihord1  39239  dihord2a  39240  dihord2b  39241  dihord2cN  39242  dihord11b  39243  dihord11c  39245  dihord2pre  39246  dihord2pre2  39247  dib2dim  39264  dih2dimb  39265  dihvalcq2  39268  dihopelvalcpre  39269  dihord6apre  39277  dihord5b  39280  dihord6b  39281  dihord5apre  39283  dih11  39286  dihwN  39310  dihmeetlem1N  39311  dihglblem5apreN  39312  dihglblem2N  39315  dihglblem3N  39316  dihmeetlem2N  39320  dihglbcpreN  39321  dihmeetbclemN  39325  dihmeetlem3N  39326  dihmeetlem4preN  39327  dihmeetlem6  39330  dihmeetlem7N  39331  dihjatc1  39332  dihjatc2N  39333  dihjatc3  39334  dihmeetlem9N  39336  dihmeetlem10N  39337  dihmeetlem11N  39338  dihmeetlem15N  39342  dihmeetlem16N  39343  dihmeetlem17N  39344  dihmeetlem19N  39346  dihmeetlem20N  39347  dihmeetALTN  39348  dihmeet2  39367  djhljjN  39423  djhj  39425  dihjatcclem1  39439  dihjatcclem2  39440  dihjatcclem4  39442  dihprrnlem1N  39445  dihprrnlem2  39446  dihjat6  39455  dihjat5N  39458  dvh4dimat  39459