Theorem hllatd 39347

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

Syntax hints:   → wi 4   ∈ wcel 2109  Latclat 18337  HLchlt 39333

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-dm 5629  df-iota 6438  df-fv 6490  df-ov 7352  df-atl 39281  df-cvlat 39305  df-hlat 39334

This theorem is referenced by:  hlrelat  39385  hlrelat2  39386  exatleN  39387  intnatN  39390  hlrelat3  39395  cvrval3  39396  cvrexchlem  39402  lnnat  39410  2atlt  39422  atexchcvrN  39423  atbtwn  39429  4noncolr3  39436  athgt  39439  3dim0  39440  3dimlem3a  39443  3dimlem4a  39446  3dim3  39452  1cvratex  39456  1cvrjat  39458  hlatexch4  39464  ps-2b  39465  3atlem1  39466  3atlem2  39467  3atlem4  39469  3atlem5  39470  3atlem6  39471  2llnmat  39507  2at0mat0  39508  2atm  39510  ps-2c  39511  llnmlplnN  39522  lplnle  39523  2atmat  39544  lplnexllnN  39547  2llnjaN  39549  lvoli3  39560  lvoli2  39564  lvolnle3at  39565  islvol2aN  39575  4atlem3  39579  4atlem3a  39580  4atlem3b  39581  4atlem4a  39582  4atlem4b  39583  4atlem4c  39584  4atlem4d  39585  4atlem9  39586  4atlem10a  39587  4atlem10  39589  4atlem11a  39590  4atlem11b  39591  4atlem11  39592  4atlem12a  39593  4atlem12b  39594  4atlem12  39595  4at  39596  4at2  39597  lplncvrlvol2  39598  lplncvrlvol  39599  2lplnja  39602  dalemkelat  39607  lneq2at  39761  lncmp  39766  2lnat  39767  cdlema1N  39774  cdlemblem  39776  cdlemb  39777  paddasslem2  39804  paddasslem5  39807  paddasslem8  39810  paddasslem12  39814  paddasslem13  39815  paddasslem15  39817  pmodlem1  39829  pmodlem2  39830  atmod1i1m  39841  llnmod1i2  39843  llnmod2i2  39846  llnexchb2lem  39851  llnexchb2  39852  dalawlem1  39854  dalawlem2  39855  dalawlem3  39856  dalawlem4  39857  dalawlem5  39858  dalawlem6  39859  dalawlem7  39860  dalawlem8  39861  dalawlem9  39862  dalawlem11  39864  dalawlem12  39865  dalawlem15  39868  pclfinclN  39933  poml4N  39936  osumcllem5N  39943  osumcllem7N  39945  pexmidlem2N  39954  pexmidlem4N  39956  pl42lem1N  39962  pl42lem2N  39963  pl42lem4N  39965  pl42N  39966  lhp2lt  39984  lhpexle2lem  39992  lhpexle3lem  39994  lhpj1  40005  lhpmcvr3  40008  lhpmcvr4N  40009  lhpmcvr5N  40010  lhpmcvr6N  40011  lhp2at0  40015  lhp2atnle  40016  lhpelim  40020  lhpmod2i2  40021  lhpmod6i1  40022  lhprelat3N  40023  lhple  40025  lhpat3  40029  4atexlemkl  40040  ltrnm  40114  ltrnj  40115  ltrnel  40122  ltrncnvel  40125  trljat1  40149  trljat2  40150  trlval3  40170  arglem1N  40173  cdlemc1  40174  cdlemc2  40175  cdlemc4  40177  cdlemc5  40178  cdlemc6  40179  cdlemd2  40182  cdlemd3  40183  cdlemd4  40184  cdlemd7  40187  cdleme0aa  40193  cdleme0b  40195  cdleme0c  40196  cdleme0e  40200  cdleme0fN  40201  cdlemeulpq  40203  cdleme01N  40204  cdleme0ex1N  40206  cdleme3g  40217  cdleme3h  40218  cdleme3  40220  cdleme4a  40222  cdleme5  40223  cdleme7aa  40225  cdleme7c  40228  cdleme7d  40229  cdleme7e  40230  cdleme7ga  40231  cdleme7  40232  cdleme8  40233  cdleme9  40236  cdleme10  40237  cdleme11c  40244  cdleme11e  40246  cdleme11fN  40247  cdleme11g  40248  cdleme11k  40251  cdleme11  40253  cdleme13  40255  cdleme15b  40258  cdleme15d  40260  cdleme15  40261  cdleme16b  40262  cdleme16e  40265  cdleme16f  40266  cdleme17b  40270  cdleme17c  40271  cdleme22gb  40277  cdlemednpq  40282  cdleme19b  40287  cdleme19c  40288  cdleme19e  40290  cdleme20aN  40292  cdleme20bN  40293  cdleme20c  40294  cdleme20d  40295  cdleme20e  40296  cdleme20j  40301  cdleme20k  40302  cdleme20l2  40304  cdleme20l  40305  cdleme20m  40306  cdleme21c  40310  cdleme21ct  40312  cdleme22aa  40322  cdleme22b  40324  cdleme22cN  40325  cdleme22d  40326  cdleme22e  40327  cdleme22eALTN  40328  cdleme22f  40329  cdleme22g  40331  cdleme23a  40332  cdleme23b  40333  cdleme23c  40334  cdleme27N  40352  cdleme28a  40353  cdleme28b  40354  cdleme29ex  40357  cdleme30a  40361  cdlemefr29exN  40385  cdleme32b  40425  cdleme32c  40426  cdleme32e  40428  cdleme35a  40431  cdleme35fnpq  40432  cdleme35b  40433  cdleme35c  40434  cdleme35d  40435  cdleme35f  40437  cdleme42c  40455  cdleme42e  40462  cdleme42h  40465  cdleme42i  40466  cdleme42mgN  40471  cdleme48bw  40485  cdlemeg46frv  40508  cdlemeg46vrg  40510  cdlemeg46rgv  40511  cdlemeg46req  40512  cdleme50eq  40524  cdlemf1  40544  trlord  40552  cdlemg2fv2  40583  cdlemg2m  40587  cdlemg7fvbwN  40590  cdlemg4c  40595  cdlemg4  40600  cdlemg6c  40603  cdlemg8b  40611  cdlemg10bALTN  40619  cdlemg10c  40622  cdlemg10  40624  cdlemg11b  40625  cdlemg12f  40631  cdlemg12g  40632  cdlemg12  40633  cdlemg13a  40634  cdlemg17a  40644  cdlemg17dALTN  40647  cdlemg17  40660  cdlemg18b  40662  cdlemg19a  40666  cdlemg19  40667  cdlemg27a  40675  cdlemg27b  40679  cdlemg31a  40680  cdlemg31b  40681  cdlemg33b0  40684  cdlemg33a  40689  cdlemg35  40696  trlcolem  40709  cdlemg42  40712  cdlemg44a  40714  cdlemg46  40718  trljco  40723  trljco2  40724  tendococl  40755  tendopltp  40763  cdlemh1  40798  cdlemh2  40799  cdlemi1  40801  cdlemi  40803  cdlemk3  40816  cdlemk4  40817  cdlemkvcl  40825  cdlemk10  40826  cdlemk7  40831  cdlemk11  40832  cdlemk12  40833  cdlemkole  40836  cdlemk14  40837  cdlemk15  40838  cdlemk1u  40842  cdlemk5u  40844  cdlemk7u  40853  cdlemk11u  40854  cdlemk12u  40855  cdlemk37  40897  cdlemk39  40899  cdlemkid1  40905  cdlemkid2  40907  cdlemk48  40933  cdlemk50  40935  cdlemk51  40936  cdlemk52  40937  cdlemk39u  40951  dia11N  41031  dia2dimlem1  41047  dia2dimlem2  41048  dia2dimlem3  41049  dia2dimlem10  41056  dia2dimlem12  41058  cdlemm10N  41101  dib11N  41143  diblss  41153  cdlemn2  41178  cdlemn10  41189  dihjustlem  41199  dihord1  41201  dihord2a  41202  dihord2b  41203  dihord2cN  41204  dihord11b  41205  dihord11c  41207  dihord2pre  41208  dihord2pre2  41209  dib2dim  41226  dih2dimb  41227  dihvalcq2  41230  dihopelvalcpre  41231  dihord6apre  41239  dihord5b  41242  dihord6b  41243  dihord5apre  41245  dih11  41248  dihwN  41272  dihmeetlem1N  41273  dihglblem5apreN  41274  dihglblem2N  41277  dihglblem3N  41278  dihmeetlem2N  41282  dihglbcpreN  41283  dihmeetbclemN  41287  dihmeetlem3N  41288  dihmeetlem4preN  41289  dihmeetlem6  41292  dihmeetlem7N  41293  dihjatc1  41294  dihjatc2N  41295  dihjatc3  41296  dihmeetlem9N  41298  dihmeetlem10N  41299  dihmeetlem11N  41300  dihmeetlem15N  41304  dihmeetlem16N  41305  dihmeetlem17N  41306  dihmeetlem19N  41308  dihmeetlem20N  41309  dihmeetALTN  41310  dihmeet2  41329  djhljjN  41385  djhj  41387  dihjatcclem1  41401  dihjatcclem2  41402  dihjatcclem4  41404  dihprrnlem1N  41407  dihprrnlem2  41408  dihjat6  41417  dihjat5N  41420  dvh4dimat  41421