Theorem hllatd 40198

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Latclat 18511  HLchlt 40184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-dm 5673  df-iota 6496  df-fv 6548  df-ov 7422  df-atl 40132  df-cvlat 40156  df-hlat 40185

This theorem is used by:  hlrelat  40236  hlrelat2  40237  exatleN  40238  intnatN  40241  hlrelat3  40246  cvrval3  40247  cvrexchlem  40253  lnnat  40261  2atlt  40273  atexchcvrN  40274  atbtwn  40280  4noncolr3  40287  athgt  40290  3dim0  40291  3dimlem3a  40294  3dimlem4a  40297  3dim3  40303  1cvratex  40307  1cvrjat  40309  hlatexch4  40315  ps-2b  40316  3atlem1  40317  3atlem2  40318  3atlem4  40320  3atlem5  40321  3atlem6  40322  2llnmat  40358  2at0mat0  40359  2atm  40361  ps-2c  40362  llnmlplnN  40373  lplnle  40374  2atmat  40395  lplnexllnN  40398  2llnjaN  40400  lvoli3  40411  lvoli2  40415  lvolnle3at  40416  islvol2aN  40426  4atlem3  40430  4atlem3a  40431  4atlem3b  40432  4atlem4a  40433  4atlem4b  40434  4atlem4c  40435  4atlem4d  40436  4atlem9  40437  4atlem10a  40438  4atlem10  40440  4atlem11a  40441  4atlem11b  40442  4atlem11  40443  4atlem12a  40444  4atlem12b  40445  4atlem12  40446  4at  40447  4at2  40448  lplncvrlvol2  40449  lplncvrlvol  40450  2lplnja  40453  dalemkelat  40458  lneq2at  40612  lncmp  40617  2lnat  40618  cdlema1N  40625  cdlemblem  40627  cdlemb  40628  paddasslem2  40655  paddasslem5  40658  paddasslem8  40661  paddasslem12  40665  paddasslem13  40666  paddasslem15  40668  pmodlem1  40680  pmodlem2  40681  atmod1i1m  40692  llnmod1i2  40694  llnmod2i2  40697  llnexchb2lem  40702  llnexchb2  40703  dalawlem1  40705  dalawlem2  40706  dalawlem3  40707  dalawlem4  40708  dalawlem5  40709  dalawlem6  40710  dalawlem7  40711  dalawlem8  40712  dalawlem9  40713  dalawlem11  40715  dalawlem12  40716  dalawlem15  40719  pclfinclN  40784  poml4N  40787  osumcllem5N  40794  osumcllem7N  40796  pexmidlem2N  40805  pexmidlem4N  40807  pl42lem1N  40813  pl42lem2N  40814  pl42lem4N  40816  pl42N  40817  lhp2lt  40835  lhpexle2lem  40843  lhpexle3lem  40845  lhpj1  40856  lhpmcvr3  40859  lhpmcvr4N  40860  lhpmcvr5N  40861  lhpmcvr6N  40862  lhp2at0  40866  lhp2atnle  40867  lhpelim  40871  lhpmod2i2  40872  lhpmod6i1  40873  lhprelat3N  40874  lhple  40876  lhpat3  40880  4atexlemkl  40891  ltrnm  40965  ltrnj  40966  ltrnel  40973  ltrncnvel  40976  trljat1  41000  trljat2  41001  trlval3  41021  arglem1N  41024  cdlemc1  41025  cdlemc2  41026  cdlemc4  41028  cdlemc5  41029  cdlemc6  41030  cdlemd2  41033  cdlemd3  41034  cdlemd4  41035  cdlemd7  41038  cdleme0aa  41044  cdleme0b  41046  cdleme0c  41047  cdleme0e  41051  cdleme0fN  41052  cdlemeulpq  41054  cdleme01N  41055  cdleme0ex1N  41057  cdleme3g  41068  cdleme3h  41069  cdleme3  41071  cdleme4a  41073  cdleme5  41074  cdleme7aa  41076  cdleme7c  41079  cdleme7d  41080  cdleme7e  41081  cdleme7ga  41082  cdleme7  41083  cdleme8  41084  cdleme9  41087  cdleme10  41088  cdleme11c  41095  cdleme11e  41097  cdleme11fN  41098  cdleme11g  41099  cdleme11k  41102  cdleme11  41104  cdleme13  41106  cdleme15b  41109  cdleme15d  41111  cdleme15  41112  cdleme16b  41113  cdleme16e  41116  cdleme16f  41117  cdleme17b  41121  cdleme17c  41122  cdleme22gb  41128  cdlemednpq  41133  cdleme19b  41138  cdleme19c  41139  cdleme19e  41141  cdleme20aN  41143  cdleme20bN  41144  cdleme20c  41145  cdleme20d  41146  cdleme20e  41147  cdleme20j  41152  cdleme20k  41153  cdleme20l2  41155  cdleme20l  41156  cdleme20m  41157  cdleme21c  41161  cdleme21ct  41163  cdleme22aa  41173  cdleme22b  41175  cdleme22cN  41176  cdleme22d  41177  cdleme22e  41178  cdleme22eALTN  41179  cdleme22f  41180  cdleme22g  41182  cdleme23a  41183  cdleme23b  41184  cdleme23c  41185  cdleme27N  41203  cdleme28a  41204  cdleme28b  41205  cdleme29ex  41208  cdleme30a  41212  cdlemefr29exN  41236  cdleme32b  41276  cdleme32c  41277  cdleme32e  41279  cdleme35a  41282  cdleme35fnpq  41283  cdleme35b  41284  cdleme35c  41285  cdleme35d  41286  cdleme35f  41288  cdleme42c  41306  cdleme42e  41313  cdleme42h  41316  cdleme42i  41317  cdleme42mgN  41322  cdleme48bw  41336  cdlemeg46frv  41359  cdlemeg46vrg  41361  cdlemeg46rgv  41362  cdlemeg46req  41363  cdleme50eq  41375  cdlemf1  41395  trlord  41403  cdlemg2fv2  41434  cdlemg2m  41438  cdlemg7fvbwN  41441  cdlemg4c  41446  cdlemg4  41451  cdlemg6c  41454  cdlemg8b  41462  cdlemg10bALTN  41470  cdlemg10c  41473  cdlemg10  41475  cdlemg11b  41476  cdlemg12f  41482  cdlemg12g  41483  cdlemg12  41484  cdlemg13a  41485  cdlemg17a  41495  cdlemg17dALTN  41498  cdlemg17  41511  cdlemg18b  41513  cdlemg19a  41517  cdlemg19  41518  cdlemg27a  41526  cdlemg27b  41530  cdlemg31a  41531  cdlemg31b  41532  cdlemg33b0  41535  cdlemg33a  41540  cdlemg35  41547  trlcolem  41560  cdlemg42  41563  cdlemg44a  41565  cdlemg46  41569  trljco  41574  trljco2  41575  tendococl  41606  tendopltp  41614  cdlemh1  41649  cdlemh2  41650  cdlemi1  41652  cdlemi  41654  cdlemk3  41667  cdlemk4  41668  cdlemkvcl  41676  cdlemk10  41677  cdlemk7  41682  cdlemk11  41683  cdlemk12  41684  cdlemkole  41687  cdlemk14  41688  cdlemk15  41689  cdlemk1u  41693  cdlemk5u  41695  cdlemk7u  41704  cdlemk11u  41705  cdlemk12u  41706  cdlemk37  41748  cdlemk39  41750  cdlemkid1  41756  cdlemkid2  41758  cdlemk48  41784  cdlemk50  41786  cdlemk51  41787  cdlemk52  41788  cdlemk39u  41802  dia11N  41882  dia2dimlem1  41898  dia2dimlem2  41899  dia2dimlem3  41900  dia2dimlem10  41907  dia2dimlem12  41909  cdlemm10N  41952  dib11N  41994  diblss  42004  cdlemn2  42029  cdlemn10  42040  dihjustlem  42050  dihord1  42052  dihord2a  42053  dihord2b  42054  dihord2cN  42055  dihord11b  42056  dihord11c  42058  dihord2pre  42059  dihord2pre2  42060  dib2dim  42077  dih2dimb  42078  dihvalcq2  42081  dihopelvalcpre  42082  dihord6apre  42090  dihord5b  42093  dihord6b  42094  dihord5apre  42096  dih11  42099  dihwN  42123  dihmeetlem1N  42124  dihglblem5apreN  42125  dihglblem2N  42128  dihglblem3N  42129  dihmeetlem2N  42133  dihglbcpreN  42134  dihmeetbclemN  42138  dihmeetlem3N  42139  dihmeetlem4preN  42140  dihmeetlem6  42143  dihmeetlem7N  42144  dihjatc1  42145  dihjatc2N  42146  dihjatc3  42147  dihmeetlem9N  42149  dihmeetlem10N  42150  dihmeetlem11N  42151  dihmeetlem15N  42155  dihmeetlem16N  42156  dihmeetlem17N  42157  dihmeetlem19N  42159  dihmeetlem20N  42160  dihmeetALTN  42161  dihmeet2  42180  djhljjN  42236  djhj  42238  dihjatcclem1  42252  dihjatcclem2  42253  dihjatcclem4  42255  dihprrnlem1N  42258  dihprrnlem2  42259  dihjat6  42268  dihjat5N  42271  dvh4dimat  42272