Theorem hllatd 40238

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Latclat 18520  HLchlt 40224

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-dm 5665  df-iota 6489  df-fv 6541  df-ov 7417  df-atl 40172  df-cvlat 40196  df-hlat 40225

This theorem is used by:  hlrelat  40276  hlrelat2  40277  exatleN  40278  intnatN  40281  hlrelat3  40286  cvrval3  40287  cvrexchlem  40293  lnnat  40301  2atlt  40313  atexchcvrN  40314  atbtwn  40320  4noncolr3  40327  athgt  40330  3dim0  40331  3dimlem3a  40334  3dimlem4a  40337  3dim3  40343  1cvratex  40347  1cvrjat  40349  hlatexch4  40355  ps-2b  40356  3atlem1  40357  3atlem2  40358  3atlem4  40360  3atlem5  40361  3atlem6  40362  2llnmat  40398  2at0mat0  40399  2atm  40401  ps-2c  40402  llnmlplnN  40413  lplnle  40414  2atmat  40435  lplnexllnN  40438  2llnjaN  40440  lvoli3  40451  lvoli2  40455  lvolnle3at  40456  islvol2aN  40466  4atlem3  40470  4atlem3a  40471  4atlem3b  40472  4atlem4a  40473  4atlem4b  40474  4atlem4c  40475  4atlem4d  40476  4atlem9  40477  4atlem10a  40478  4atlem10  40480  4atlem11a  40481  4atlem11b  40482  4atlem11  40483  4atlem12a  40484  4atlem12b  40485  4atlem12  40486  4at  40487  4at2  40488  lplncvrlvol2  40489  lplncvrlvol  40490  2lplnja  40493  dalemkelat  40498  lneq2at  40652  lncmp  40657  2lnat  40658  cdlema1N  40665  cdlemblem  40667  cdlemb  40668  paddasslem2  40695  paddasslem5  40698  paddasslem8  40701  paddasslem12  40705  paddasslem13  40706  paddasslem15  40708  pmodlem1  40720  pmodlem2  40721  atmod1i1m  40732  llnmod1i2  40734  llnmod2i2  40737  llnexchb2lem  40742  llnexchb2  40743  dalawlem1  40745  dalawlem2  40746  dalawlem3  40747  dalawlem4  40748  dalawlem5  40749  dalawlem6  40750  dalawlem7  40751  dalawlem8  40752  dalawlem9  40753  dalawlem11  40755  dalawlem12  40756  dalawlem15  40759  pclfinclN  40824  poml4N  40827  osumcllem5N  40834  osumcllem7N  40836  pexmidlem2N  40845  pexmidlem4N  40847  pl42lem1N  40853  pl42lem2N  40854  pl42lem4N  40856  pl42N  40857  lhp2lt  40875  lhpexle2lem  40883  lhpexle3lem  40885  lhpj1  40896  lhpmcvr3  40899  lhpmcvr4N  40900  lhpmcvr5N  40901  lhpmcvr6N  40902  lhp2at0  40906  lhp2atnle  40907  lhpelim  40911  lhpmod2i2  40912  lhpmod6i1  40913  lhprelat3N  40914  lhple  40916  lhpat3  40920  4atexlemkl  40931  ltrnm  41005  ltrnj  41006  ltrnel  41013  ltrncnvel  41016  trljat1  41040  trljat2  41041  trlval3  41061  arglem1N  41064  cdlemc1  41065  cdlemc2  41066  cdlemc4  41068  cdlemc5  41069  cdlemc6  41070  cdlemd2  41073  cdlemd3  41074  cdlemd4  41075  cdlemd7  41078  cdleme0aa  41084  cdleme0b  41086  cdleme0c  41087  cdleme0e  41091  cdleme0fN  41092  cdlemeulpq  41094  cdleme01N  41095  cdleme0ex1N  41097  cdleme3g  41108  cdleme3h  41109  cdleme3  41111  cdleme4a  41113  cdleme5  41114  cdleme7aa  41116  cdleme7c  41119  cdleme7d  41120  cdleme7e  41121  cdleme7ga  41122  cdleme7  41123  cdleme8  41124  cdleme9  41127  cdleme10  41128  cdleme11c  41135  cdleme11e  41137  cdleme11fN  41138  cdleme11g  41139  cdleme11k  41142  cdleme11  41144  cdleme13  41146  cdleme15b  41149  cdleme15d  41151  cdleme15  41152  cdleme16b  41153  cdleme16e  41156  cdleme16f  41157  cdleme17b  41161  cdleme17c  41162  cdleme22gb  41168  cdlemednpq  41173  cdleme19b  41178  cdleme19c  41179  cdleme19e  41181  cdleme20aN  41183  cdleme20bN  41184  cdleme20c  41185  cdleme20d  41186  cdleme20e  41187  cdleme20j  41192  cdleme20k  41193  cdleme20l2  41195  cdleme20l  41196  cdleme20m  41197  cdleme21c  41201  cdleme21ct  41203  cdleme22aa  41213  cdleme22b  41215  cdleme22cN  41216  cdleme22d  41217  cdleme22e  41218  cdleme22eALTN  41219  cdleme22f  41220  cdleme22g  41222  cdleme23a  41223  cdleme23b  41224  cdleme23c  41225  cdleme27N  41243  cdleme28a  41244  cdleme28b  41245  cdleme29ex  41248  cdleme30a  41252  cdlemefr29exN  41276  cdleme32b  41316  cdleme32c  41317  cdleme32e  41319  cdleme35a  41322  cdleme35fnpq  41323  cdleme35b  41324  cdleme35c  41325  cdleme35d  41326  cdleme35f  41328  cdleme42c  41346  cdleme42e  41353  cdleme42h  41356  cdleme42i  41357  cdleme42mgN  41362  cdleme48bw  41376  cdlemeg46frv  41399  cdlemeg46vrg  41401  cdlemeg46rgv  41402  cdlemeg46req  41403  cdleme50eq  41415  cdlemf1  41435  trlord  41443  cdlemg2fv2  41474  cdlemg2m  41478  cdlemg7fvbwN  41481  cdlemg4c  41486  cdlemg4  41491  cdlemg6c  41494  cdlemg8b  41502  cdlemg10bALTN  41510  cdlemg10c  41513  cdlemg10  41515  cdlemg11b  41516  cdlemg12f  41522  cdlemg12g  41523  cdlemg12  41524  cdlemg13a  41525  cdlemg17a  41535  cdlemg17dALTN  41538  cdlemg17  41551  cdlemg18b  41553  cdlemg19a  41557  cdlemg19  41558  cdlemg27a  41566  cdlemg27b  41570  cdlemg31a  41571  cdlemg31b  41572  cdlemg33b0  41575  cdlemg33a  41580  cdlemg35  41587  trlcolem  41600  cdlemg42  41603  cdlemg44a  41605  cdlemg46  41609  trljco  41614  trljco2  41615  tendococl  41646  tendopltp  41654  cdlemh1  41689  cdlemh2  41690  cdlemi1  41692  cdlemi  41694  cdlemk3  41707  cdlemk4  41708  cdlemkvcl  41716  cdlemk10  41717  cdlemk7  41722  cdlemk11  41723  cdlemk12  41724  cdlemkole  41727  cdlemk14  41728  cdlemk15  41729  cdlemk1u  41733  cdlemk5u  41735  cdlemk7u  41744  cdlemk11u  41745  cdlemk12u  41746  cdlemk37  41788  cdlemk39  41790  cdlemkid1  41796  cdlemkid2  41798  cdlemk48  41824  cdlemk50  41826  cdlemk51  41827  cdlemk52  41828  cdlemk39u  41842  dia11N  41922  dia2dimlem1  41938  dia2dimlem2  41939  dia2dimlem3  41940  dia2dimlem10  41947  dia2dimlem12  41949  cdlemm10N  41992  dib11N  42034  diblss  42044  cdlemn2  42069  cdlemn10  42080  dihjustlem  42090  dihord1  42092  dihord2a  42093  dihord2b  42094  dihord2cN  42095  dihord11b  42096  dihord11c  42098  dihord2pre  42099  dihord2pre2  42100  dib2dim  42117  dih2dimb  42118  dihvalcq2  42121  dihopelvalcpre  42122  dihord6apre  42130  dihord5b  42133  dihord6b  42134  dihord5apre  42136  dih11  42139  dihwN  42163  dihmeetlem1N  42164  dihglblem5apreN  42165  dihglblem2N  42168  dihglblem3N  42169  dihmeetlem2N  42173  dihglbcpreN  42174  dihmeetbclemN  42178  dihmeetlem3N  42179  dihmeetlem4preN  42180  dihmeetlem6  42183  dihmeetlem7N  42184  dihjatc1  42185  dihjatc2N  42186  dihjatc3  42187  dihmeetlem9N  42189  dihmeetlem10N  42190  dihmeetlem11N  42191  dihmeetlem15N  42195  dihmeetlem16N  42196  dihmeetlem17N  42197  dihmeetlem19N  42199  dihmeetlem20N  42200  dihmeetALTN  42201  dihmeet2  42220  djhljjN  42276  djhj  42278  dihjatcclem1  42292  dihjatcclem2  42293  dihjatcclem4  42295  dihprrnlem1N  42298  dihprrnlem2  42299  dihjat6  42308  dihjat5N  42311  dvh4dimat  42312