Theorem hllatd 35163

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

Syntax hints:   → wi 4   ∈ wcel 2157  Latclat 17270  HLchlt 35149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-dm 5334  df-iota 6074  df-fv 6119  df-ov 6887  df-atl 35097  df-cvlat 35121  df-hlat 35150

This theorem is referenced by:  hlrelat  35201  hlrelat2  35202  exatleN  35203  intnatN  35206  hlrelat3  35211  cvrval3  35212  cvrexchlem  35218  lnnat  35226  2atlt  35238  atexchcvrN  35239  atbtwn  35245  4noncolr3  35252  athgt  35255  3dim0  35256  3dimlem3a  35259  3dimlem4a  35262  3dim3  35268  1cvratex  35272  1cvrjat  35274  hlatexch4  35280  ps-2b  35281  3atlem1  35282  3atlem2  35283  3atlem4  35285  3atlem5  35286  3atlem6  35287  2llnmat  35323  2at0mat0  35324  2atm  35326  ps-2c  35327  llnmlplnN  35338  lplnle  35339  2atmat  35360  lplnexllnN  35363  2llnjaN  35365  lvoli3  35376  lvoli2  35380  lvolnle3at  35381  islvol2aN  35391  4atlem3  35395  4atlem3a  35396  4atlem3b  35397  4atlem4a  35398  4atlem4b  35399  4atlem4c  35400  4atlem4d  35401  4atlem9  35402  4atlem10a  35403  4atlem10  35405  4atlem11a  35406  4atlem11b  35407  4atlem11  35408  4atlem12a  35409  4atlem12b  35410  4atlem12  35411  4at  35412  4at2  35413  lplncvrlvol2  35414  lplncvrlvol  35415  2lplnja  35418  dalemkelat  35423  lneq2at  35577  lncmp  35582  2lnat  35583  cdlema1N  35590  cdlemblem  35592  cdlemb  35593  paddasslem2  35620  paddasslem5  35623  paddasslem8  35626  paddasslem12  35630  paddasslem13  35631  paddasslem15  35633  pmodlem1  35645  pmodlem2  35646  atmod1i1m  35657  llnmod1i2  35659  llnmod2i2  35662  llnexchb2lem  35667  llnexchb2  35668  dalawlem1  35670  dalawlem2  35671  dalawlem3  35672  dalawlem4  35673  dalawlem5  35674  dalawlem6  35675  dalawlem7  35676  dalawlem8  35677  dalawlem9  35678  dalawlem11  35680  dalawlem12  35681  dalawlem15  35684  pclfinclN  35749  poml4N  35752  osumcllem5N  35759  osumcllem7N  35761  pexmidlem2N  35770  pexmidlem4N  35772  pl42lem1N  35778  pl42lem2N  35779  pl42lem4N  35781  pl42N  35782  lhp2lt  35800  lhpexle2lem  35808  lhpexle3lem  35810  lhpj1  35821  lhpmcvr3  35824  lhpmcvr4N  35825  lhpmcvr5N  35826  lhpmcvr6N  35827  lhp2at0  35831  lhp2atnle  35832  lhpelim  35836  lhpmod2i2  35837  lhpmod6i1  35838  lhprelat3N  35839  lhple  35841  lhpat3  35845  4atexlemkl  35856  ltrnm  35930  ltrnj  35931  ltrnel  35938  ltrncnvel  35941  trljat1  35965  trljat2  35966  trlval3  35986  arglem1N  35989  cdlemc1  35990  cdlemc2  35991  cdlemc4  35993  cdlemc5  35994  cdlemc6  35995  cdlemd2  35998  cdlemd3  35999  cdlemd4  36000  cdlemd7  36003  cdleme0aa  36009  cdleme0b  36011  cdleme0c  36012  cdleme0e  36016  cdleme0fN  36017  cdlemeulpq  36019  cdleme01N  36020  cdleme0ex1N  36022  cdleme3g  36033  cdleme3h  36034  cdleme3  36036  cdleme4a  36038  cdleme5  36039  cdleme7aa  36041  cdleme7c  36044  cdleme7d  36045  cdleme7e  36046  cdleme7ga  36047  cdleme7  36048  cdleme8  36049  cdleme9  36052  cdleme10  36053  cdleme11c  36060  cdleme11e  36062  cdleme11fN  36063  cdleme11g  36064  cdleme11k  36067  cdleme11  36069  cdleme13  36071  cdleme15b  36074  cdleme15d  36076  cdleme15  36077  cdleme16b  36078  cdleme16e  36081  cdleme16f  36082  cdleme17b  36086  cdleme17c  36087  cdleme22gb  36093  cdlemednpq  36098  cdleme19b  36103  cdleme19c  36104  cdleme19e  36106  cdleme20aN  36108  cdleme20bN  36109  cdleme20c  36110  cdleme20d  36111  cdleme20e  36112  cdleme20j  36117  cdleme20k  36118  cdleme20l2  36120  cdleme20l  36121  cdleme20m  36122  cdleme21c  36126  cdleme21ct  36128  cdleme22aa  36138  cdleme22b  36140  cdleme22cN  36141  cdleme22d  36142  cdleme22e  36143  cdleme22eALTN  36144  cdleme22f  36145  cdleme22g  36147  cdleme23a  36148  cdleme23b  36149  cdleme23c  36150  cdleme27N  36168  cdleme28a  36169  cdleme28b  36170  cdleme29ex  36173  cdleme30a  36177  cdlemefr29exN  36201  cdleme32b  36241  cdleme32c  36242  cdleme32e  36244  cdleme35a  36247  cdleme35fnpq  36248  cdleme35b  36249  cdleme35c  36250  cdleme35d  36251  cdleme35f  36253  cdleme42c  36271  cdleme42e  36278  cdleme42h  36281  cdleme42i  36282  cdleme42mgN  36287  cdleme48bw  36301  cdlemeg46frv  36324  cdlemeg46vrg  36326  cdlemeg46rgv  36327  cdlemeg46req  36328  cdleme50eq  36340  cdlemf1  36360  trlord  36368  cdlemg2fv2  36399  cdlemg2m  36403  cdlemg7fvbwN  36406  cdlemg4c  36411  cdlemg4  36416  cdlemg6c  36419  cdlemg8b  36427  cdlemg10bALTN  36435  cdlemg10c  36438  cdlemg10  36440  cdlemg11b  36441  cdlemg12f  36447  cdlemg12g  36448  cdlemg12  36449  cdlemg13a  36450  cdlemg17a  36460  cdlemg17dALTN  36463  cdlemg17  36476  cdlemg18b  36478  cdlemg19a  36482  cdlemg19  36483  cdlemg27a  36491  cdlemg27b  36495  cdlemg31a  36496  cdlemg31b  36497  cdlemg33b0  36500  cdlemg33a  36505  cdlemg35  36512  trlcolem  36525  cdlemg42  36528  cdlemg44a  36530  cdlemg46  36534  trljco  36539  trljco2  36540  tendococl  36571  tendopltp  36579  cdlemh1  36614  cdlemh2  36615  cdlemi1  36617  cdlemi  36619  cdlemk3  36632  cdlemk4  36633  cdlemkvcl  36641  cdlemk10  36642  cdlemk7  36647  cdlemk11  36648  cdlemk12  36649  cdlemkole  36652  cdlemk14  36653  cdlemk15  36654  cdlemk1u  36658  cdlemk5u  36660  cdlemk7u  36669  cdlemk11u  36670  cdlemk12u  36671  cdlemk37  36713  cdlemk39  36715  cdlemkid1  36721  cdlemkid2  36723  cdlemk48  36749  cdlemk50  36751  cdlemk51  36752  cdlemk52  36753  cdlemk39u  36767  dia11N  36847  dia2dimlem1  36863  dia2dimlem2  36864  dia2dimlem3  36865  dia2dimlem10  36872  dia2dimlem12  36874  cdlemm10N  36917  dib11N  36959  diblss  36969  cdlemn2  36994  cdlemn10  37005  dihjustlem  37015  dihord1  37017  dihord2a  37018  dihord2b  37019  dihord2cN  37020  dihord11b  37021  dihord11c  37023  dihord2pre  37024  dihord2pre2  37025  dib2dim  37042  dih2dimb  37043  dihvalcq2  37046  dihopelvalcpre  37047  dihord6apre  37055  dihord5b  37058  dihord6b  37059  dihord5apre  37061  dih11  37064  dihwN  37088  dihmeetlem1N  37089  dihglblem5apreN  37090  dihglblem2N  37093  dihglblem3N  37094  dihmeetlem2N  37098  dihglbcpreN  37099  dihmeetbclemN  37103  dihmeetlem3N  37104  dihmeetlem4preN  37105  dihmeetlem6  37108  dihmeetlem7N  37109  dihjatc1  37110  dihjatc2N  37111  dihjatc3  37112  dihmeetlem9N  37114  dihmeetlem10N  37115  dihmeetlem11N  37116  dihmeetlem15N  37120  dihmeetlem16N  37121  dihmeetlem17N  37122  dihmeetlem19N  37124  dihmeetlem20N  37125  dihmeetALTN  37126  dihmeet2  37145  djhljjN  37201  djhj  37203  dihjatcclem1  37217  dihjatcclem2  37218  dihjatcclem4  37220  dihprrnlem1N  37223  dihprrnlem2  37224  dihjat6  37233  dihjat5N  37236  dvh4dimat  37237