Theorem hllatd 39634

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

Syntax hints:   → wi 4   ∈ wcel 2113  Latclat 18354  HLchlt 39620

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-dm 5634  df-iota 6448  df-fv 6500  df-ov 7361  df-atl 39568  df-cvlat 39592  df-hlat 39621

This theorem is referenced by:  hlrelat  39672  hlrelat2  39673  exatleN  39674  intnatN  39677  hlrelat3  39682  cvrval3  39683  cvrexchlem  39689  lnnat  39697  2atlt  39709  atexchcvrN  39710  atbtwn  39716  4noncolr3  39723  athgt  39726  3dim0  39727  3dimlem3a  39730  3dimlem4a  39733  3dim3  39739  1cvratex  39743  1cvrjat  39745  hlatexch4  39751  ps-2b  39752  3atlem1  39753  3atlem2  39754  3atlem4  39756  3atlem5  39757  3atlem6  39758  2llnmat  39794  2at0mat0  39795  2atm  39797  ps-2c  39798  llnmlplnN  39809  lplnle  39810  2atmat  39831  lplnexllnN  39834  2llnjaN  39836  lvoli3  39847  lvoli2  39851  lvolnle3at  39852  islvol2aN  39862  4atlem3  39866  4atlem3a  39867  4atlem3b  39868  4atlem4a  39869  4atlem4b  39870  4atlem4c  39871  4atlem4d  39872  4atlem9  39873  4atlem10a  39874  4atlem10  39876  4atlem11a  39877  4atlem11b  39878  4atlem11  39879  4atlem12a  39880  4atlem12b  39881  4atlem12  39882  4at  39883  4at2  39884  lplncvrlvol2  39885  lplncvrlvol  39886  2lplnja  39889  dalemkelat  39894  lneq2at  40048  lncmp  40053  2lnat  40054  cdlema1N  40061  cdlemblem  40063  cdlemb  40064  paddasslem2  40091  paddasslem5  40094  paddasslem8  40097  paddasslem12  40101  paddasslem13  40102  paddasslem15  40104  pmodlem1  40116  pmodlem2  40117  atmod1i1m  40128  llnmod1i2  40130  llnmod2i2  40133  llnexchb2lem  40138  llnexchb2  40139  dalawlem1  40141  dalawlem2  40142  dalawlem3  40143  dalawlem4  40144  dalawlem5  40145  dalawlem6  40146  dalawlem7  40147  dalawlem8  40148  dalawlem9  40149  dalawlem11  40151  dalawlem12  40152  dalawlem15  40155  pclfinclN  40220  poml4N  40223  osumcllem5N  40230  osumcllem7N  40232  pexmidlem2N  40241  pexmidlem4N  40243  pl42lem1N  40249  pl42lem2N  40250  pl42lem4N  40252  pl42N  40253  lhp2lt  40271  lhpexle2lem  40279  lhpexle3lem  40281  lhpj1  40292  lhpmcvr3  40295  lhpmcvr4N  40296  lhpmcvr5N  40297  lhpmcvr6N  40298  lhp2at0  40302  lhp2atnle  40303  lhpelim  40307  lhpmod2i2  40308  lhpmod6i1  40309  lhprelat3N  40310  lhple  40312  lhpat3  40316  4atexlemkl  40327  ltrnm  40401  ltrnj  40402  ltrnel  40409  ltrncnvel  40412  trljat1  40436  trljat2  40437  trlval3  40457  arglem1N  40460  cdlemc1  40461  cdlemc2  40462  cdlemc4  40464  cdlemc5  40465  cdlemc6  40466  cdlemd2  40469  cdlemd3  40470  cdlemd4  40471  cdlemd7  40474  cdleme0aa  40480  cdleme0b  40482  cdleme0c  40483  cdleme0e  40487  cdleme0fN  40488  cdlemeulpq  40490  cdleme01N  40491  cdleme0ex1N  40493  cdleme3g  40504  cdleme3h  40505  cdleme3  40507  cdleme4a  40509  cdleme5  40510  cdleme7aa  40512  cdleme7c  40515  cdleme7d  40516  cdleme7e  40517  cdleme7ga  40518  cdleme7  40519  cdleme8  40520  cdleme9  40523  cdleme10  40524  cdleme11c  40531  cdleme11e  40533  cdleme11fN  40534  cdleme11g  40535  cdleme11k  40538  cdleme11  40540  cdleme13  40542  cdleme15b  40545  cdleme15d  40547  cdleme15  40548  cdleme16b  40549  cdleme16e  40552  cdleme16f  40553  cdleme17b  40557  cdleme17c  40558  cdleme22gb  40564  cdlemednpq  40569  cdleme19b  40574  cdleme19c  40575  cdleme19e  40577  cdleme20aN  40579  cdleme20bN  40580  cdleme20c  40581  cdleme20d  40582  cdleme20e  40583  cdleme20j  40588  cdleme20k  40589  cdleme20l2  40591  cdleme20l  40592  cdleme20m  40593  cdleme21c  40597  cdleme21ct  40599  cdleme22aa  40609  cdleme22b  40611  cdleme22cN  40612  cdleme22d  40613  cdleme22e  40614  cdleme22eALTN  40615  cdleme22f  40616  cdleme22g  40618  cdleme23a  40619  cdleme23b  40620  cdleme23c  40621  cdleme27N  40639  cdleme28a  40640  cdleme28b  40641  cdleme29ex  40644  cdleme30a  40648  cdlemefr29exN  40672  cdleme32b  40712  cdleme32c  40713  cdleme32e  40715  cdleme35a  40718  cdleme35fnpq  40719  cdleme35b  40720  cdleme35c  40721  cdleme35d  40722  cdleme35f  40724  cdleme42c  40742  cdleme42e  40749  cdleme42h  40752  cdleme42i  40753  cdleme42mgN  40758  cdleme48bw  40772  cdlemeg46frv  40795  cdlemeg46vrg  40797  cdlemeg46rgv  40798  cdlemeg46req  40799  cdleme50eq  40811  cdlemf1  40831  trlord  40839  cdlemg2fv2  40870  cdlemg2m  40874  cdlemg7fvbwN  40877  cdlemg4c  40882  cdlemg4  40887  cdlemg6c  40890  cdlemg8b  40898  cdlemg10bALTN  40906  cdlemg10c  40909  cdlemg10  40911  cdlemg11b  40912  cdlemg12f  40918  cdlemg12g  40919  cdlemg12  40920  cdlemg13a  40921  cdlemg17a  40931  cdlemg17dALTN  40934  cdlemg17  40947  cdlemg18b  40949  cdlemg19a  40953  cdlemg19  40954  cdlemg27a  40962  cdlemg27b  40966  cdlemg31a  40967  cdlemg31b  40968  cdlemg33b0  40971  cdlemg33a  40976  cdlemg35  40983  trlcolem  40996  cdlemg42  40999  cdlemg44a  41001  cdlemg46  41005  trljco  41010  trljco2  41011  tendococl  41042  tendopltp  41050  cdlemh1  41085  cdlemh2  41086  cdlemi1  41088  cdlemi  41090  cdlemk3  41103  cdlemk4  41104  cdlemkvcl  41112  cdlemk10  41113  cdlemk7  41118  cdlemk11  41119  cdlemk12  41120  cdlemkole  41123  cdlemk14  41124  cdlemk15  41125  cdlemk1u  41129  cdlemk5u  41131  cdlemk7u  41140  cdlemk11u  41141  cdlemk12u  41142  cdlemk37  41184  cdlemk39  41186  cdlemkid1  41192  cdlemkid2  41194  cdlemk48  41220  cdlemk50  41222  cdlemk51  41223  cdlemk52  41224  cdlemk39u  41238  dia11N  41318  dia2dimlem1  41334  dia2dimlem2  41335  dia2dimlem3  41336  dia2dimlem10  41343  dia2dimlem12  41345  cdlemm10N  41388  dib11N  41430  diblss  41440  cdlemn2  41465  cdlemn10  41476  dihjustlem  41486  dihord1  41488  dihord2a  41489  dihord2b  41490  dihord2cN  41491  dihord11b  41492  dihord11c  41494  dihord2pre  41495  dihord2pre2  41496  dib2dim  41513  dih2dimb  41514  dihvalcq2  41517  dihopelvalcpre  41518  dihord6apre  41526  dihord5b  41529  dihord6b  41530  dihord5apre  41532  dih11  41535  dihwN  41559  dihmeetlem1N  41560  dihglblem5apreN  41561  dihglblem2N  41564  dihglblem3N  41565  dihmeetlem2N  41569  dihglbcpreN  41570  dihmeetbclemN  41574  dihmeetlem3N  41575  dihmeetlem4preN  41576  dihmeetlem6  41579  dihmeetlem7N  41580  dihjatc1  41581  dihjatc2N  41582  dihjatc3  41583  dihmeetlem9N  41585  dihmeetlem10N  41586  dihmeetlem11N  41587  dihmeetlem15N  41591  dihmeetlem16N  41592  dihmeetlem17N  41593  dihmeetlem19N  41595  dihmeetlem20N  41596  dihmeetALTN  41597  dihmeet2  41616  djhljjN  41672  djhj  41674  dihjatcclem1  41688  dihjatcclem2  41689  dihjatcclem4  41691  dihprrnlem1N  41694  dihprrnlem2  41695  dihjat6  41704  dihjat5N  41707  dvh4dimat  41708