Theorem hllatd 36504

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

Syntax hints:   → wi 4   ∈ wcel 2113  Latclat 17658  HLchlt 36490

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-dm 5568  df-iota 6317  df-fv 6366  df-ov 7162  df-atl 36438  df-cvlat 36462  df-hlat 36491

This theorem is referenced by:  hlrelat  36542  hlrelat2  36543  exatleN  36544  intnatN  36547  hlrelat3  36552  cvrval3  36553  cvrexchlem  36559  lnnat  36567  2atlt  36579  atexchcvrN  36580  atbtwn  36586  4noncolr3  36593  athgt  36596  3dim0  36597  3dimlem3a  36600  3dimlem4a  36603  3dim3  36609  1cvratex  36613  1cvrjat  36615  hlatexch4  36621  ps-2b  36622  3atlem1  36623  3atlem2  36624  3atlem4  36626  3atlem5  36627  3atlem6  36628  2llnmat  36664  2at0mat0  36665  2atm  36667  ps-2c  36668  llnmlplnN  36679  lplnle  36680  2atmat  36701  lplnexllnN  36704  2llnjaN  36706  lvoli3  36717  lvoli2  36721  lvolnle3at  36722  islvol2aN  36732  4atlem3  36736  4atlem3a  36737  4atlem3b  36738  4atlem4a  36739  4atlem4b  36740  4atlem4c  36741  4atlem4d  36742  4atlem9  36743  4atlem10a  36744  4atlem10  36746  4atlem11a  36747  4atlem11b  36748  4atlem11  36749  4atlem12a  36750  4atlem12b  36751  4atlem12  36752  4at  36753  4at2  36754  lplncvrlvol2  36755  lplncvrlvol  36756  2lplnja  36759  dalemkelat  36764  lneq2at  36918  lncmp  36923  2lnat  36924  cdlema1N  36931  cdlemblem  36933  cdlemb  36934  paddasslem2  36961  paddasslem5  36964  paddasslem8  36967  paddasslem12  36971  paddasslem13  36972  paddasslem15  36974  pmodlem1  36986  pmodlem2  36987  atmod1i1m  36998  llnmod1i2  37000  llnmod2i2  37003  llnexchb2lem  37008  llnexchb2  37009  dalawlem1  37011  dalawlem2  37012  dalawlem3  37013  dalawlem4  37014  dalawlem5  37015  dalawlem6  37016  dalawlem7  37017  dalawlem8  37018  dalawlem9  37019  dalawlem11  37021  dalawlem12  37022  dalawlem15  37025  pclfinclN  37090  poml4N  37093  osumcllem5N  37100  osumcllem7N  37102  pexmidlem2N  37111  pexmidlem4N  37113  pl42lem1N  37119  pl42lem2N  37120  pl42lem4N  37122  pl42N  37123  lhp2lt  37141  lhpexle2lem  37149  lhpexle3lem  37151  lhpj1  37162  lhpmcvr3  37165  lhpmcvr4N  37166  lhpmcvr5N  37167  lhpmcvr6N  37168  lhp2at0  37172  lhp2atnle  37173  lhpelim  37177  lhpmod2i2  37178  lhpmod6i1  37179  lhprelat3N  37180  lhple  37182  lhpat3  37186  4atexlemkl  37197  ltrnm  37271  ltrnj  37272  ltrnel  37279  ltrncnvel  37282  trljat1  37306  trljat2  37307  trlval3  37327  arglem1N  37330  cdlemc1  37331  cdlemc2  37332  cdlemc4  37334  cdlemc5  37335  cdlemc6  37336  cdlemd2  37339  cdlemd3  37340  cdlemd4  37341  cdlemd7  37344  cdleme0aa  37350  cdleme0b  37352  cdleme0c  37353  cdleme0e  37357  cdleme0fN  37358  cdlemeulpq  37360  cdleme01N  37361  cdleme0ex1N  37363  cdleme3g  37374  cdleme3h  37375  cdleme3  37377  cdleme4a  37379  cdleme5  37380  cdleme7aa  37382  cdleme7c  37385  cdleme7d  37386  cdleme7e  37387  cdleme7ga  37388  cdleme7  37389  cdleme8  37390  cdleme9  37393  cdleme10  37394  cdleme11c  37401  cdleme11e  37403  cdleme11fN  37404  cdleme11g  37405  cdleme11k  37408  cdleme11  37410  cdleme13  37412  cdleme15b  37415  cdleme15d  37417  cdleme15  37418  cdleme16b  37419  cdleme16e  37422  cdleme16f  37423  cdleme17b  37427  cdleme17c  37428  cdleme22gb  37434  cdlemednpq  37439  cdleme19b  37444  cdleme19c  37445  cdleme19e  37447  cdleme20aN  37449  cdleme20bN  37450  cdleme20c  37451  cdleme20d  37452  cdleme20e  37453  cdleme20j  37458  cdleme20k  37459  cdleme20l2  37461  cdleme20l  37462  cdleme20m  37463  cdleme21c  37467  cdleme21ct  37469  cdleme22aa  37479  cdleme22b  37481  cdleme22cN  37482  cdleme22d  37483  cdleme22e  37484  cdleme22eALTN  37485  cdleme22f  37486  cdleme22g  37488  cdleme23a  37489  cdleme23b  37490  cdleme23c  37491  cdleme27N  37509  cdleme28a  37510  cdleme28b  37511  cdleme29ex  37514  cdleme30a  37518  cdlemefr29exN  37542  cdleme32b  37582  cdleme32c  37583  cdleme32e  37585  cdleme35a  37588  cdleme35fnpq  37589  cdleme35b  37590  cdleme35c  37591  cdleme35d  37592  cdleme35f  37594  cdleme42c  37612  cdleme42e  37619  cdleme42h  37622  cdleme42i  37623  cdleme42mgN  37628  cdleme48bw  37642  cdlemeg46frv  37665  cdlemeg46vrg  37667  cdlemeg46rgv  37668  cdlemeg46req  37669  cdleme50eq  37681  cdlemf1  37701  trlord  37709  cdlemg2fv2  37740  cdlemg2m  37744  cdlemg7fvbwN  37747  cdlemg4c  37752  cdlemg4  37757  cdlemg6c  37760  cdlemg8b  37768  cdlemg10bALTN  37776  cdlemg10c  37779  cdlemg10  37781  cdlemg11b  37782  cdlemg12f  37788  cdlemg12g  37789  cdlemg12  37790  cdlemg13a  37791  cdlemg17a  37801  cdlemg17dALTN  37804  cdlemg17  37817  cdlemg18b  37819  cdlemg19a  37823  cdlemg19  37824  cdlemg27a  37832  cdlemg27b  37836  cdlemg31a  37837  cdlemg31b  37838  cdlemg33b0  37841  cdlemg33a  37846  cdlemg35  37853  trlcolem  37866  cdlemg42  37869  cdlemg44a  37871  cdlemg46  37875  trljco  37880  trljco2  37881  tendococl  37912  tendopltp  37920  cdlemh1  37955  cdlemh2  37956  cdlemi1  37958  cdlemi  37960  cdlemk3  37973  cdlemk4  37974  cdlemkvcl  37982  cdlemk10  37983  cdlemk7  37988  cdlemk11  37989  cdlemk12  37990  cdlemkole  37993  cdlemk14  37994  cdlemk15  37995  cdlemk1u  37999  cdlemk5u  38001  cdlemk7u  38010  cdlemk11u  38011  cdlemk12u  38012  cdlemk37  38054  cdlemk39  38056  cdlemkid1  38062  cdlemkid2  38064  cdlemk48  38090  cdlemk50  38092  cdlemk51  38093  cdlemk52  38094  cdlemk39u  38108  dia11N  38188  dia2dimlem1  38204  dia2dimlem2  38205  dia2dimlem3  38206  dia2dimlem10  38213  dia2dimlem12  38215  cdlemm10N  38258  dib11N  38300  diblss  38310  cdlemn2  38335  cdlemn10  38346  dihjustlem  38356  dihord1  38358  dihord2a  38359  dihord2b  38360  dihord2cN  38361  dihord11b  38362  dihord11c  38364  dihord2pre  38365  dihord2pre2  38366  dib2dim  38383  dih2dimb  38384  dihvalcq2  38387  dihopelvalcpre  38388  dihord6apre  38396  dihord5b  38399  dihord6b  38400  dihord5apre  38402  dih11  38405  dihwN  38429  dihmeetlem1N  38430  dihglblem5apreN  38431  dihglblem2N  38434  dihglblem3N  38435  dihmeetlem2N  38439  dihglbcpreN  38440  dihmeetbclemN  38444  dihmeetlem3N  38445  dihmeetlem4preN  38446  dihmeetlem6  38449  dihmeetlem7N  38450  dihjatc1  38451  dihjatc2N  38452  dihjatc3  38453  dihmeetlem9N  38455  dihmeetlem10N  38456  dihmeetlem11N  38457  dihmeetlem15N  38461  dihmeetlem16N  38462  dihmeetlem17N  38463  dihmeetlem19N  38465  dihmeetlem20N  38466  dihmeetALTN  38467  dihmeet2  38486  djhljjN  38542  djhj  38544  dihjatcclem1  38558  dihjatcclem2  38559  dihjatcclem4  38561  dihprrnlem1N  38564  dihprrnlem2  38565  dihjat6  38574  dihjat5N  38577  dvh4dimat  38578