Theorem hllatd 38234

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

Syntax hints:   → wi 4   ∈ wcel 2107  Latclat 18384  HLchlt 38220

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-dm 5687  df-iota 6496  df-fv 6552  df-ov 7412  df-atl 38168  df-cvlat 38192  df-hlat 38221

This theorem is referenced by:  hlrelat  38273  hlrelat2  38274  exatleN  38275  intnatN  38278  hlrelat3  38283  cvrval3  38284  cvrexchlem  38290  lnnat  38298  2atlt  38310  atexchcvrN  38311  atbtwn  38317  4noncolr3  38324  athgt  38327  3dim0  38328  3dimlem3a  38331  3dimlem4a  38334  3dim3  38340  1cvratex  38344  1cvrjat  38346  hlatexch4  38352  ps-2b  38353  3atlem1  38354  3atlem2  38355  3atlem4  38357  3atlem5  38358  3atlem6  38359  2llnmat  38395  2at0mat0  38396  2atm  38398  ps-2c  38399  llnmlplnN  38410  lplnle  38411  2atmat  38432  lplnexllnN  38435  2llnjaN  38437  lvoli3  38448  lvoli2  38452  lvolnle3at  38453  islvol2aN  38463  4atlem3  38467  4atlem3a  38468  4atlem3b  38469  4atlem4a  38470  4atlem4b  38471  4atlem4c  38472  4atlem4d  38473  4atlem9  38474  4atlem10a  38475  4atlem10  38477  4atlem11a  38478  4atlem11b  38479  4atlem11  38480  4atlem12a  38481  4atlem12b  38482  4atlem12  38483  4at  38484  4at2  38485  lplncvrlvol2  38486  lplncvrlvol  38487  2lplnja  38490  dalemkelat  38495  lneq2at  38649  lncmp  38654  2lnat  38655  cdlema1N  38662  cdlemblem  38664  cdlemb  38665  paddasslem2  38692  paddasslem5  38695  paddasslem8  38698  paddasslem12  38702  paddasslem13  38703  paddasslem15  38705  pmodlem1  38717  pmodlem2  38718  atmod1i1m  38729  llnmod1i2  38731  llnmod2i2  38734  llnexchb2lem  38739  llnexchb2  38740  dalawlem1  38742  dalawlem2  38743  dalawlem3  38744  dalawlem4  38745  dalawlem5  38746  dalawlem6  38747  dalawlem7  38748  dalawlem8  38749  dalawlem9  38750  dalawlem11  38752  dalawlem12  38753  dalawlem15  38756  pclfinclN  38821  poml4N  38824  osumcllem5N  38831  osumcllem7N  38833  pexmidlem2N  38842  pexmidlem4N  38844  pl42lem1N  38850  pl42lem2N  38851  pl42lem4N  38853  pl42N  38854  lhp2lt  38872  lhpexle2lem  38880  lhpexle3lem  38882  lhpj1  38893  lhpmcvr3  38896  lhpmcvr4N  38897  lhpmcvr5N  38898  lhpmcvr6N  38899  lhp2at0  38903  lhp2atnle  38904  lhpelim  38908  lhpmod2i2  38909  lhpmod6i1  38910  lhprelat3N  38911  lhple  38913  lhpat3  38917  4atexlemkl  38928  ltrnm  39002  ltrnj  39003  ltrnel  39010  ltrncnvel  39013  trljat1  39037  trljat2  39038  trlval3  39058  arglem1N  39061  cdlemc1  39062  cdlemc2  39063  cdlemc4  39065  cdlemc5  39066  cdlemc6  39067  cdlemd2  39070  cdlemd3  39071  cdlemd4  39072  cdlemd7  39075  cdleme0aa  39081  cdleme0b  39083  cdleme0c  39084  cdleme0e  39088  cdleme0fN  39089  cdlemeulpq  39091  cdleme01N  39092  cdleme0ex1N  39094  cdleme3g  39105  cdleme3h  39106  cdleme3  39108  cdleme4a  39110  cdleme5  39111  cdleme7aa  39113  cdleme7c  39116  cdleme7d  39117  cdleme7e  39118  cdleme7ga  39119  cdleme7  39120  cdleme8  39121  cdleme9  39124  cdleme10  39125  cdleme11c  39132  cdleme11e  39134  cdleme11fN  39135  cdleme11g  39136  cdleme11k  39139  cdleme11  39141  cdleme13  39143  cdleme15b  39146  cdleme15d  39148  cdleme15  39149  cdleme16b  39150  cdleme16e  39153  cdleme16f  39154  cdleme17b  39158  cdleme17c  39159  cdleme22gb  39165  cdlemednpq  39170  cdleme19b  39175  cdleme19c  39176  cdleme19e  39178  cdleme20aN  39180  cdleme20bN  39181  cdleme20c  39182  cdleme20d  39183  cdleme20e  39184  cdleme20j  39189  cdleme20k  39190  cdleme20l2  39192  cdleme20l  39193  cdleme20m  39194  cdleme21c  39198  cdleme21ct  39200  cdleme22aa  39210  cdleme22b  39212  cdleme22cN  39213  cdleme22d  39214  cdleme22e  39215  cdleme22eALTN  39216  cdleme22f  39217  cdleme22g  39219  cdleme23a  39220  cdleme23b  39221  cdleme23c  39222  cdleme27N  39240  cdleme28a  39241  cdleme28b  39242  cdleme29ex  39245  cdleme30a  39249  cdlemefr29exN  39273  cdleme32b  39313  cdleme32c  39314  cdleme32e  39316  cdleme35a  39319  cdleme35fnpq  39320  cdleme35b  39321  cdleme35c  39322  cdleme35d  39323  cdleme35f  39325  cdleme42c  39343  cdleme42e  39350  cdleme42h  39353  cdleme42i  39354  cdleme42mgN  39359  cdleme48bw  39373  cdlemeg46frv  39396  cdlemeg46vrg  39398  cdlemeg46rgv  39399  cdlemeg46req  39400  cdleme50eq  39412  cdlemf1  39432  trlord  39440  cdlemg2fv2  39471  cdlemg2m  39475  cdlemg7fvbwN  39478  cdlemg4c  39483  cdlemg4  39488  cdlemg6c  39491  cdlemg8b  39499  cdlemg10bALTN  39507  cdlemg10c  39510  cdlemg10  39512  cdlemg11b  39513  cdlemg12f  39519  cdlemg12g  39520  cdlemg12  39521  cdlemg13a  39522  cdlemg17a  39532  cdlemg17dALTN  39535  cdlemg17  39548  cdlemg18b  39550  cdlemg19a  39554  cdlemg19  39555  cdlemg27a  39563  cdlemg27b  39567  cdlemg31a  39568  cdlemg31b  39569  cdlemg33b0  39572  cdlemg33a  39577  cdlemg35  39584  trlcolem  39597  cdlemg42  39600  cdlemg44a  39602  cdlemg46  39606  trljco  39611  trljco2  39612  tendococl  39643  tendopltp  39651  cdlemh1  39686  cdlemh2  39687  cdlemi1  39689  cdlemi  39691  cdlemk3  39704  cdlemk4  39705  cdlemkvcl  39713  cdlemk10  39714  cdlemk7  39719  cdlemk11  39720  cdlemk12  39721  cdlemkole  39724  cdlemk14  39725  cdlemk15  39726  cdlemk1u  39730  cdlemk5u  39732  cdlemk7u  39741  cdlemk11u  39742  cdlemk12u  39743  cdlemk37  39785  cdlemk39  39787  cdlemkid1  39793  cdlemkid2  39795  cdlemk48  39821  cdlemk50  39823  cdlemk51  39824  cdlemk52  39825  cdlemk39u  39839  dia11N  39919  dia2dimlem1  39935  dia2dimlem2  39936  dia2dimlem3  39937  dia2dimlem10  39944  dia2dimlem12  39946  cdlemm10N  39989  dib11N  40031  diblss  40041  cdlemn2  40066  cdlemn10  40077  dihjustlem  40087  dihord1  40089  dihord2a  40090  dihord2b  40091  dihord2cN  40092  dihord11b  40093  dihord11c  40095  dihord2pre  40096  dihord2pre2  40097  dib2dim  40114  dih2dimb  40115  dihvalcq2  40118  dihopelvalcpre  40119  dihord6apre  40127  dihord5b  40130  dihord6b  40131  dihord5apre  40133  dih11  40136  dihwN  40160  dihmeetlem1N  40161  dihglblem5apreN  40162  dihglblem2N  40165  dihglblem3N  40166  dihmeetlem2N  40170  dihglbcpreN  40171  dihmeetbclemN  40175  dihmeetlem3N  40176  dihmeetlem4preN  40177  dihmeetlem6  40180  dihmeetlem7N  40181  dihjatc1  40182  dihjatc2N  40183  dihjatc3  40184  dihmeetlem9N  40186  dihmeetlem10N  40187  dihmeetlem11N  40188  dihmeetlem15N  40192  dihmeetlem16N  40193  dihmeetlem17N  40194  dihmeetlem19N  40196  dihmeetlem20N  40197  dihmeetALTN  40198  dihmeet2  40217  djhljjN  40273  djhj  40275  dihjatcclem1  40289  dihjatcclem2  40290  dihjatcclem4  40292  dihprrnlem1N  40295  dihprrnlem2  40296  dihjat6  40305  dihjat5N  40308  dvh4dimat  40309