Theorem hllatd 39827

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

Syntax hints:   → wi 4   ∈ wcel 2114  Latclat 18391  HLchlt 39813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-dm 5635  df-iota 6449  df-fv 6501  df-ov 7364  df-atl 39761  df-cvlat 39785  df-hlat 39814

This theorem is referenced by:  hlrelat  39865  hlrelat2  39866  exatleN  39867  intnatN  39870  hlrelat3  39875  cvrval3  39876  cvrexchlem  39882  lnnat  39890  2atlt  39902  atexchcvrN  39903  atbtwn  39909  4noncolr3  39916  athgt  39919  3dim0  39920  3dimlem3a  39923  3dimlem4a  39926  3dim3  39932  1cvratex  39936  1cvrjat  39938  hlatexch4  39944  ps-2b  39945  3atlem1  39946  3atlem2  39947  3atlem4  39949  3atlem5  39950  3atlem6  39951  2llnmat  39987  2at0mat0  39988  2atm  39990  ps-2c  39991  llnmlplnN  40002  lplnle  40003  2atmat  40024  lplnexllnN  40027  2llnjaN  40029  lvoli3  40040  lvoli2  40044  lvolnle3at  40045  islvol2aN  40055  4atlem3  40059  4atlem3a  40060  4atlem3b  40061  4atlem4a  40062  4atlem4b  40063  4atlem4c  40064  4atlem4d  40065  4atlem9  40066  4atlem10a  40067  4atlem10  40069  4atlem11a  40070  4atlem11b  40071  4atlem11  40072  4atlem12a  40073  4atlem12b  40074  4atlem12  40075  4at  40076  4at2  40077  lplncvrlvol2  40078  lplncvrlvol  40079  2lplnja  40082  dalemkelat  40087  lneq2at  40241  lncmp  40246  2lnat  40247  cdlema1N  40254  cdlemblem  40256  cdlemb  40257  paddasslem2  40284  paddasslem5  40287  paddasslem8  40290  paddasslem12  40294  paddasslem13  40295  paddasslem15  40297  pmodlem1  40309  pmodlem2  40310  atmod1i1m  40321  llnmod1i2  40323  llnmod2i2  40326  llnexchb2lem  40331  llnexchb2  40332  dalawlem1  40334  dalawlem2  40335  dalawlem3  40336  dalawlem4  40337  dalawlem5  40338  dalawlem6  40339  dalawlem7  40340  dalawlem8  40341  dalawlem9  40342  dalawlem11  40344  dalawlem12  40345  dalawlem15  40348  pclfinclN  40413  poml4N  40416  osumcllem5N  40423  osumcllem7N  40425  pexmidlem2N  40434  pexmidlem4N  40436  pl42lem1N  40442  pl42lem2N  40443  pl42lem4N  40445  pl42N  40446  lhp2lt  40464  lhpexle2lem  40472  lhpexle3lem  40474  lhpj1  40485  lhpmcvr3  40488  lhpmcvr4N  40489  lhpmcvr5N  40490  lhpmcvr6N  40491  lhp2at0  40495  lhp2atnle  40496  lhpelim  40500  lhpmod2i2  40501  lhpmod6i1  40502  lhprelat3N  40503  lhple  40505  lhpat3  40509  4atexlemkl  40520  ltrnm  40594  ltrnj  40595  ltrnel  40602  ltrncnvel  40605  trljat1  40629  trljat2  40630  trlval3  40650  arglem1N  40653  cdlemc1  40654  cdlemc2  40655  cdlemc4  40657  cdlemc5  40658  cdlemc6  40659  cdlemd2  40662  cdlemd3  40663  cdlemd4  40664  cdlemd7  40667  cdleme0aa  40673  cdleme0b  40675  cdleme0c  40676  cdleme0e  40680  cdleme0fN  40681  cdlemeulpq  40683  cdleme01N  40684  cdleme0ex1N  40686  cdleme3g  40697  cdleme3h  40698  cdleme3  40700  cdleme4a  40702  cdleme5  40703  cdleme7aa  40705  cdleme7c  40708  cdleme7d  40709  cdleme7e  40710  cdleme7ga  40711  cdleme7  40712  cdleme8  40713  cdleme9  40716  cdleme10  40717  cdleme11c  40724  cdleme11e  40726  cdleme11fN  40727  cdleme11g  40728  cdleme11k  40731  cdleme11  40733  cdleme13  40735  cdleme15b  40738  cdleme15d  40740  cdleme15  40741  cdleme16b  40742  cdleme16e  40745  cdleme16f  40746  cdleme17b  40750  cdleme17c  40751  cdleme22gb  40757  cdlemednpq  40762  cdleme19b  40767  cdleme19c  40768  cdleme19e  40770  cdleme20aN  40772  cdleme20bN  40773  cdleme20c  40774  cdleme20d  40775  cdleme20e  40776  cdleme20j  40781  cdleme20k  40782  cdleme20l2  40784  cdleme20l  40785  cdleme20m  40786  cdleme21c  40790  cdleme21ct  40792  cdleme22aa  40802  cdleme22b  40804  cdleme22cN  40805  cdleme22d  40806  cdleme22e  40807  cdleme22eALTN  40808  cdleme22f  40809  cdleme22g  40811  cdleme23a  40812  cdleme23b  40813  cdleme23c  40814  cdleme27N  40832  cdleme28a  40833  cdleme28b  40834  cdleme29ex  40837  cdleme30a  40841  cdlemefr29exN  40865  cdleme32b  40905  cdleme32c  40906  cdleme32e  40908  cdleme35a  40911  cdleme35fnpq  40912  cdleme35b  40913  cdleme35c  40914  cdleme35d  40915  cdleme35f  40917  cdleme42c  40935  cdleme42e  40942  cdleme42h  40945  cdleme42i  40946  cdleme42mgN  40951  cdleme48bw  40965  cdlemeg46frv  40988  cdlemeg46vrg  40990  cdlemeg46rgv  40991  cdlemeg46req  40992  cdleme50eq  41004  cdlemf1  41024  trlord  41032  cdlemg2fv2  41063  cdlemg2m  41067  cdlemg7fvbwN  41070  cdlemg4c  41075  cdlemg4  41080  cdlemg6c  41083  cdlemg8b  41091  cdlemg10bALTN  41099  cdlemg10c  41102  cdlemg10  41104  cdlemg11b  41105  cdlemg12f  41111  cdlemg12g  41112  cdlemg12  41113  cdlemg13a  41114  cdlemg17a  41124  cdlemg17dALTN  41127  cdlemg17  41140  cdlemg18b  41142  cdlemg19a  41146  cdlemg19  41147  cdlemg27a  41155  cdlemg27b  41159  cdlemg31a  41160  cdlemg31b  41161  cdlemg33b0  41164  cdlemg33a  41169  cdlemg35  41176  trlcolem  41189  cdlemg42  41192  cdlemg44a  41194  cdlemg46  41198  trljco  41203  trljco2  41204  tendococl  41235  tendopltp  41243  cdlemh1  41278  cdlemh2  41279  cdlemi1  41281  cdlemi  41283  cdlemk3  41296  cdlemk4  41297  cdlemkvcl  41305  cdlemk10  41306  cdlemk7  41311  cdlemk11  41312  cdlemk12  41313  cdlemkole  41316  cdlemk14  41317  cdlemk15  41318  cdlemk1u  41322  cdlemk5u  41324  cdlemk7u  41333  cdlemk11u  41334  cdlemk12u  41335  cdlemk37  41377  cdlemk39  41379  cdlemkid1  41385  cdlemkid2  41387  cdlemk48  41413  cdlemk50  41415  cdlemk51  41416  cdlemk52  41417  cdlemk39u  41431  dia11N  41511  dia2dimlem1  41527  dia2dimlem2  41528  dia2dimlem3  41529  dia2dimlem10  41536  dia2dimlem12  41538  cdlemm10N  41581  dib11N  41623  diblss  41633  cdlemn2  41658  cdlemn10  41669  dihjustlem  41679  dihord1  41681  dihord2a  41682  dihord2b  41683  dihord2cN  41684  dihord11b  41685  dihord11c  41687  dihord2pre  41688  dihord2pre2  41689  dib2dim  41706  dih2dimb  41707  dihvalcq2  41710  dihopelvalcpre  41711  dihord6apre  41719  dihord5b  41722  dihord6b  41723  dihord5apre  41725  dih11  41728  dihwN  41752  dihmeetlem1N  41753  dihglblem5apreN  41754  dihglblem2N  41757  dihglblem3N  41758  dihmeetlem2N  41762  dihglbcpreN  41763  dihmeetbclemN  41767  dihmeetlem3N  41768  dihmeetlem4preN  41769  dihmeetlem6  41772  dihmeetlem7N  41773  dihjatc1  41774  dihjatc2N  41775  dihjatc3  41776  dihmeetlem9N  41778  dihmeetlem10N  41779  dihmeetlem11N  41780  dihmeetlem15N  41784  dihmeetlem16N  41785  dihmeetlem17N  41786  dihmeetlem19N  41788  dihmeetlem20N  41789  dihmeetALTN  41790  dihmeet2  41809  djhljjN  41865  djhj  41867  dihjatcclem1  41881  dihjatcclem2  41882  dihjatcclem4  41884  dihprrnlem1N  41887  dihprrnlem2  41888  dihjat6  41897  dihjat5N  41900  dvh4dimat  41901