Theorem hllatd 39357

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

Syntax hints:   → wi 4   ∈ wcel 2109  Latclat 18390  HLchlt 39343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-dm 5648  df-iota 6464  df-fv 6519  df-ov 7390  df-atl 39291  df-cvlat 39315  df-hlat 39344

This theorem is referenced by:  hlrelat  39396  hlrelat2  39397  exatleN  39398  intnatN  39401  hlrelat3  39406  cvrval3  39407  cvrexchlem  39413  lnnat  39421  2atlt  39433  atexchcvrN  39434  atbtwn  39440  4noncolr3  39447  athgt  39450  3dim0  39451  3dimlem3a  39454  3dimlem4a  39457  3dim3  39463  1cvratex  39467  1cvrjat  39469  hlatexch4  39475  ps-2b  39476  3atlem1  39477  3atlem2  39478  3atlem4  39480  3atlem5  39481  3atlem6  39482  2llnmat  39518  2at0mat0  39519  2atm  39521  ps-2c  39522  llnmlplnN  39533  lplnle  39534  2atmat  39555  lplnexllnN  39558  2llnjaN  39560  lvoli3  39571  lvoli2  39575  lvolnle3at  39576  islvol2aN  39586  4atlem3  39590  4atlem3a  39591  4atlem3b  39592  4atlem4a  39593  4atlem4b  39594  4atlem4c  39595  4atlem4d  39596  4atlem9  39597  4atlem10a  39598  4atlem10  39600  4atlem11a  39601  4atlem11b  39602  4atlem11  39603  4atlem12a  39604  4atlem12b  39605  4atlem12  39606  4at  39607  4at2  39608  lplncvrlvol2  39609  lplncvrlvol  39610  2lplnja  39613  dalemkelat  39618  lneq2at  39772  lncmp  39777  2lnat  39778  cdlema1N  39785  cdlemblem  39787  cdlemb  39788  paddasslem2  39815  paddasslem5  39818  paddasslem8  39821  paddasslem12  39825  paddasslem13  39826  paddasslem15  39828  pmodlem1  39840  pmodlem2  39841  atmod1i1m  39852  llnmod1i2  39854  llnmod2i2  39857  llnexchb2lem  39862  llnexchb2  39863  dalawlem1  39865  dalawlem2  39866  dalawlem3  39867  dalawlem4  39868  dalawlem5  39869  dalawlem6  39870  dalawlem7  39871  dalawlem8  39872  dalawlem9  39873  dalawlem11  39875  dalawlem12  39876  dalawlem15  39879  pclfinclN  39944  poml4N  39947  osumcllem5N  39954  osumcllem7N  39956  pexmidlem2N  39965  pexmidlem4N  39967  pl42lem1N  39973  pl42lem2N  39974  pl42lem4N  39976  pl42N  39977  lhp2lt  39995  lhpexle2lem  40003  lhpexle3lem  40005  lhpj1  40016  lhpmcvr3  40019  lhpmcvr4N  40020  lhpmcvr5N  40021  lhpmcvr6N  40022  lhp2at0  40026  lhp2atnle  40027  lhpelim  40031  lhpmod2i2  40032  lhpmod6i1  40033  lhprelat3N  40034  lhple  40036  lhpat3  40040  4atexlemkl  40051  ltrnm  40125  ltrnj  40126  ltrnel  40133  ltrncnvel  40136  trljat1  40160  trljat2  40161  trlval3  40181  arglem1N  40184  cdlemc1  40185  cdlemc2  40186  cdlemc4  40188  cdlemc5  40189  cdlemc6  40190  cdlemd2  40193  cdlemd3  40194  cdlemd4  40195  cdlemd7  40198  cdleme0aa  40204  cdleme0b  40206  cdleme0c  40207  cdleme0e  40211  cdleme0fN  40212  cdlemeulpq  40214  cdleme01N  40215  cdleme0ex1N  40217  cdleme3g  40228  cdleme3h  40229  cdleme3  40231  cdleme4a  40233  cdleme5  40234  cdleme7aa  40236  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme8  40244  cdleme9  40247  cdleme10  40248  cdleme11c  40255  cdleme11e  40257  cdleme11fN  40258  cdleme11g  40259  cdleme11k  40262  cdleme11  40264  cdleme13  40266  cdleme15b  40269  cdleme15d  40271  cdleme15  40272  cdleme16b  40273  cdleme16e  40276  cdleme16f  40277  cdleme17b  40281  cdleme17c  40282  cdleme22gb  40288  cdlemednpq  40293  cdleme19b  40298  cdleme19c  40299  cdleme19e  40301  cdleme20aN  40303  cdleme20bN  40304  cdleme20c  40305  cdleme20d  40306  cdleme20e  40307  cdleme20j  40312  cdleme20k  40313  cdleme20l2  40315  cdleme20l  40316  cdleme20m  40317  cdleme21c  40321  cdleme21ct  40323  cdleme22aa  40333  cdleme22b  40335  cdleme22cN  40336  cdleme22d  40337  cdleme22e  40338  cdleme22eALTN  40339  cdleme22f  40340  cdleme22g  40342  cdleme23a  40343  cdleme23b  40344  cdleme23c  40345  cdleme27N  40363  cdleme28a  40364  cdleme28b  40365  cdleme29ex  40368  cdleme30a  40372  cdlemefr29exN  40396  cdleme32b  40436  cdleme32c  40437  cdleme32e  40439  cdleme35a  40442  cdleme35fnpq  40443  cdleme35b  40444  cdleme35c  40445  cdleme35d  40446  cdleme35f  40448  cdleme42c  40466  cdleme42e  40473  cdleme42h  40476  cdleme42i  40477  cdleme42mgN  40482  cdleme48bw  40496  cdlemeg46frv  40519  cdlemeg46vrg  40521  cdlemeg46rgv  40522  cdlemeg46req  40523  cdleme50eq  40535  cdlemf1  40555  trlord  40563  cdlemg2fv2  40594  cdlemg2m  40598  cdlemg7fvbwN  40601  cdlemg4c  40606  cdlemg4  40611  cdlemg6c  40614  cdlemg8b  40622  cdlemg10bALTN  40630  cdlemg10c  40633  cdlemg10  40635  cdlemg11b  40636  cdlemg12f  40642  cdlemg12g  40643  cdlemg12  40644  cdlemg13a  40645  cdlemg17a  40655  cdlemg17dALTN  40658  cdlemg17  40671  cdlemg18b  40673  cdlemg19a  40677  cdlemg19  40678  cdlemg27a  40686  cdlemg27b  40690  cdlemg31a  40691  cdlemg31b  40692  cdlemg33b0  40695  cdlemg33a  40700  cdlemg35  40707  trlcolem  40720  cdlemg42  40723  cdlemg44a  40725  cdlemg46  40729  trljco  40734  trljco2  40735  tendococl  40766  tendopltp  40774  cdlemh1  40809  cdlemh2  40810  cdlemi1  40812  cdlemi  40814  cdlemk3  40827  cdlemk4  40828  cdlemkvcl  40836  cdlemk10  40837  cdlemk7  40842  cdlemk11  40843  cdlemk12  40844  cdlemkole  40847  cdlemk14  40848  cdlemk15  40849  cdlemk1u  40853  cdlemk5u  40855  cdlemk7u  40864  cdlemk11u  40865  cdlemk12u  40866  cdlemk37  40908  cdlemk39  40910  cdlemkid1  40916  cdlemkid2  40918  cdlemk48  40944  cdlemk50  40946  cdlemk51  40947  cdlemk52  40948  cdlemk39u  40962  dia11N  41042  dia2dimlem1  41058  dia2dimlem2  41059  dia2dimlem3  41060  dia2dimlem10  41067  dia2dimlem12  41069  cdlemm10N  41112  dib11N  41154  diblss  41164  cdlemn2  41189  cdlemn10  41200  dihjustlem  41210  dihord1  41212  dihord2a  41213  dihord2b  41214  dihord2cN  41215  dihord11b  41216  dihord11c  41218  dihord2pre  41219  dihord2pre2  41220  dib2dim  41237  dih2dimb  41238  dihvalcq2  41241  dihopelvalcpre  41242  dihord6apre  41250  dihord5b  41253  dihord6b  41254  dihord5apre  41256  dih11  41259  dihwN  41283  dihmeetlem1N  41284  dihglblem5apreN  41285  dihglblem2N  41288  dihglblem3N  41289  dihmeetlem2N  41293  dihglbcpreN  41294  dihmeetbclemN  41298  dihmeetlem3N  41299  dihmeetlem4preN  41300  dihmeetlem6  41303  dihmeetlem7N  41304  dihjatc1  41305  dihjatc2N  41306  dihjatc3  41307  dihmeetlem9N  41309  dihmeetlem10N  41310  dihmeetlem11N  41311  dihmeetlem15N  41315  dihmeetlem16N  41316  dihmeetlem17N  41317  dihmeetlem19N  41319  dihmeetlem20N  41320  dihmeetALTN  41321  dihmeet2  41340  djhljjN  41396  djhj  41398  dihjatcclem1  41412  dihjatcclem2  41413  dihjatcclem4  41415  dihprrnlem1N  41418  dihprrnlem2  41419  dihjat6  41428  dihjat5N  41431  dvh4dimat  41432