Theorem hllatd 39350

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

Syntax hints:   → wi 4   ∈ wcel 2109  Latclat 18372  HLchlt 39336

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-dm 5641  df-iota 6452  df-fv 6507  df-ov 7372  df-atl 39284  df-cvlat 39308  df-hlat 39337

This theorem is referenced by:  hlrelat  39389  hlrelat2  39390  exatleN  39391  intnatN  39394  hlrelat3  39399  cvrval3  39400  cvrexchlem  39406  lnnat  39414  2atlt  39426  atexchcvrN  39427  atbtwn  39433  4noncolr3  39440  athgt  39443  3dim0  39444  3dimlem3a  39447  3dimlem4a  39450  3dim3  39456  1cvratex  39460  1cvrjat  39462  hlatexch4  39468  ps-2b  39469  3atlem1  39470  3atlem2  39471  3atlem4  39473  3atlem5  39474  3atlem6  39475  2llnmat  39511  2at0mat0  39512  2atm  39514  ps-2c  39515  llnmlplnN  39526  lplnle  39527  2atmat  39548  lplnexllnN  39551  2llnjaN  39553  lvoli3  39564  lvoli2  39568  lvolnle3at  39569  islvol2aN  39579  4atlem3  39583  4atlem3a  39584  4atlem3b  39585  4atlem4a  39586  4atlem4b  39587  4atlem4c  39588  4atlem4d  39589  4atlem9  39590  4atlem10a  39591  4atlem10  39593  4atlem11a  39594  4atlem11b  39595  4atlem11  39596  4atlem12a  39597  4atlem12b  39598  4atlem12  39599  4at  39600  4at2  39601  lplncvrlvol2  39602  lplncvrlvol  39603  2lplnja  39606  dalemkelat  39611  lneq2at  39765  lncmp  39770  2lnat  39771  cdlema1N  39778  cdlemblem  39780  cdlemb  39781  paddasslem2  39808  paddasslem5  39811  paddasslem8  39814  paddasslem12  39818  paddasslem13  39819  paddasslem15  39821  pmodlem1  39833  pmodlem2  39834  atmod1i1m  39845  llnmod1i2  39847  llnmod2i2  39850  llnexchb2lem  39855  llnexchb2  39856  dalawlem1  39858  dalawlem2  39859  dalawlem3  39860  dalawlem4  39861  dalawlem5  39862  dalawlem6  39863  dalawlem7  39864  dalawlem8  39865  dalawlem9  39866  dalawlem11  39868  dalawlem12  39869  dalawlem15  39872  pclfinclN  39937  poml4N  39940  osumcllem5N  39947  osumcllem7N  39949  pexmidlem2N  39958  pexmidlem4N  39960  pl42lem1N  39966  pl42lem2N  39967  pl42lem4N  39969  pl42N  39970  lhp2lt  39988  lhpexle2lem  39996  lhpexle3lem  39998  lhpj1  40009  lhpmcvr3  40012  lhpmcvr4N  40013  lhpmcvr5N  40014  lhpmcvr6N  40015  lhp2at0  40019  lhp2atnle  40020  lhpelim  40024  lhpmod2i2  40025  lhpmod6i1  40026  lhprelat3N  40027  lhple  40029  lhpat3  40033  4atexlemkl  40044  ltrnm  40118  ltrnj  40119  ltrnel  40126  ltrncnvel  40129  trljat1  40153  trljat2  40154  trlval3  40174  arglem1N  40177  cdlemc1  40178  cdlemc2  40179  cdlemc4  40181  cdlemc5  40182  cdlemc6  40183  cdlemd2  40186  cdlemd3  40187  cdlemd4  40188  cdlemd7  40191  cdleme0aa  40197  cdleme0b  40199  cdleme0c  40200  cdleme0e  40204  cdleme0fN  40205  cdlemeulpq  40207  cdleme01N  40208  cdleme0ex1N  40210  cdleme3g  40221  cdleme3h  40222  cdleme3  40224  cdleme4a  40226  cdleme5  40227  cdleme7aa  40229  cdleme7c  40232  cdleme7d  40233  cdleme7e  40234  cdleme7ga  40235  cdleme7  40236  cdleme8  40237  cdleme9  40240  cdleme10  40241  cdleme11c  40248  cdleme11e  40250  cdleme11fN  40251  cdleme11g  40252  cdleme11k  40255  cdleme11  40257  cdleme13  40259  cdleme15b  40262  cdleme15d  40264  cdleme15  40265  cdleme16b  40266  cdleme16e  40269  cdleme16f  40270  cdleme17b  40274  cdleme17c  40275  cdleme22gb  40281  cdlemednpq  40286  cdleme19b  40291  cdleme19c  40292  cdleme19e  40294  cdleme20aN  40296  cdleme20bN  40297  cdleme20c  40298  cdleme20d  40299  cdleme20e  40300  cdleme20j  40305  cdleme20k  40306  cdleme20l2  40308  cdleme20l  40309  cdleme20m  40310  cdleme21c  40314  cdleme21ct  40316  cdleme22aa  40326  cdleme22b  40328  cdleme22cN  40329  cdleme22d  40330  cdleme22e  40331  cdleme22eALTN  40332  cdleme22f  40333  cdleme22g  40335  cdleme23a  40336  cdleme23b  40337  cdleme23c  40338  cdleme27N  40356  cdleme28a  40357  cdleme28b  40358  cdleme29ex  40361  cdleme30a  40365  cdlemefr29exN  40389  cdleme32b  40429  cdleme32c  40430  cdleme32e  40432  cdleme35a  40435  cdleme35fnpq  40436  cdleme35b  40437  cdleme35c  40438  cdleme35d  40439  cdleme35f  40441  cdleme42c  40459  cdleme42e  40466  cdleme42h  40469  cdleme42i  40470  cdleme42mgN  40475  cdleme48bw  40489  cdlemeg46frv  40512  cdlemeg46vrg  40514  cdlemeg46rgv  40515  cdlemeg46req  40516  cdleme50eq  40528  cdlemf1  40548  trlord  40556  cdlemg2fv2  40587  cdlemg2m  40591  cdlemg7fvbwN  40594  cdlemg4c  40599  cdlemg4  40604  cdlemg6c  40607  cdlemg8b  40615  cdlemg10bALTN  40623  cdlemg10c  40626  cdlemg10  40628  cdlemg11b  40629  cdlemg12f  40635  cdlemg12g  40636  cdlemg12  40637  cdlemg13a  40638  cdlemg17a  40648  cdlemg17dALTN  40651  cdlemg17  40664  cdlemg18b  40666  cdlemg19a  40670  cdlemg19  40671  cdlemg27a  40679  cdlemg27b  40683  cdlemg31a  40684  cdlemg31b  40685  cdlemg33b0  40688  cdlemg33a  40693  cdlemg35  40700  trlcolem  40713  cdlemg42  40716  cdlemg44a  40718  cdlemg46  40722  trljco  40727  trljco2  40728  tendococl  40759  tendopltp  40767  cdlemh1  40802  cdlemh2  40803  cdlemi1  40805  cdlemi  40807  cdlemk3  40820  cdlemk4  40821  cdlemkvcl  40829  cdlemk10  40830  cdlemk7  40835  cdlemk11  40836  cdlemk12  40837  cdlemkole  40840  cdlemk14  40841  cdlemk15  40842  cdlemk1u  40846  cdlemk5u  40848  cdlemk7u  40857  cdlemk11u  40858  cdlemk12u  40859  cdlemk37  40901  cdlemk39  40903  cdlemkid1  40909  cdlemkid2  40911  cdlemk48  40937  cdlemk50  40939  cdlemk51  40940  cdlemk52  40941  cdlemk39u  40955  dia11N  41035  dia2dimlem1  41051  dia2dimlem2  41052  dia2dimlem3  41053  dia2dimlem10  41060  dia2dimlem12  41062  cdlemm10N  41105  dib11N  41147  diblss  41157  cdlemn2  41182  cdlemn10  41193  dihjustlem  41203  dihord1  41205  dihord2a  41206  dihord2b  41207  dihord2cN  41208  dihord11b  41209  dihord11c  41211  dihord2pre  41212  dihord2pre2  41213  dib2dim  41230  dih2dimb  41231  dihvalcq2  41234  dihopelvalcpre  41235  dihord6apre  41243  dihord5b  41246  dihord6b  41247  dihord5apre  41249  dih11  41252  dihwN  41276  dihmeetlem1N  41277  dihglblem5apreN  41278  dihglblem2N  41281  dihglblem3N  41282  dihmeetlem2N  41286  dihglbcpreN  41287  dihmeetbclemN  41291  dihmeetlem3N  41292  dihmeetlem4preN  41293  dihmeetlem6  41296  dihmeetlem7N  41297  dihjatc1  41298  dihjatc2N  41299  dihjatc3  41300  dihmeetlem9N  41302  dihmeetlem10N  41303  dihmeetlem11N  41304  dihmeetlem15N  41308  dihmeetlem16N  41309  dihmeetlem17N  41310  dihmeetlem19N  41312  dihmeetlem20N  41313  dihmeetALTN  41314  dihmeet2  41333  djhljjN  41389  djhj  41391  dihjatcclem1  41405  dihjatcclem2  41406  dihjatcclem4  41408  dihprrnlem1N  41411  dihprrnlem2  41412  dihjat6  41421  dihjat5N  41424  dvh4dimat  41425