Theorem hllatd 40687

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Latclat 18655  HLchlt 40673

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-dm 5668  df-iota 6520  df-fv 6574  df-ov 7454  df-atl 40621  df-cvlat 40645  df-hlat 40674

This theorem is used by:  hlrelat  40725  hlrelat2  40726  exatleN  40727  intnatN  40730  hlrelat3  40735  cvrval3  40736  cvrexchlem  40742  lnnat  40750  2atlt  40762  atexchcvrN  40763  atbtwn  40769  4noncolr3  40776  athgt  40779  3dim0  40780  3dimlem3a  40783  3dimlem4a  40786  3dim3  40792  1cvratex  40796  1cvrjat  40798  hlatexch4  40804  ps-2b  40805  3atlem1  40806  3atlem2  40807  3atlem4  40809  3atlem5  40810  3atlem6  40811  2llnmat  40847  2at0mat0  40848  2atm  40850  ps-2c  40851  llnmlplnN  40862  lplnle  40863  2atmat  40884  lplnexllnN  40887  2llnjaN  40889  lvoli3  40900  lvoli2  40904  lvolnle3at  40905  islvol2aN  40915  4atlem3  40919  4atlem3a  40920  4atlem3b  40921  4atlem4a  40922  4atlem4b  40923  4atlem4c  40924  4atlem4d  40925  4atlem9  40926  4atlem10a  40927  4atlem10  40929  4atlem11a  40930  4atlem11b  40931  4atlem11  40932  4atlem12a  40933  4atlem12b  40934  4atlem12  40935  4at  40936  4at2  40937  lplncvrlvol2  40938  lplncvrlvol  40939  2lplnja  40942  dalemkelat  40947  lneq2at  41101  lncmp  41106  2lnat  41107  cdlema1N  41114  cdlemblem  41116  cdlemb  41117  paddasslem2  41144  paddasslem5  41147  paddasslem8  41150  paddasslem12  41154  paddasslem13  41155  paddasslem15  41157  pmodlem1  41169  pmodlem2  41170  atmod1i1m  41181  llnmod1i2  41183  llnmod2i2  41186  llnexchb2lem  41191  llnexchb2  41192  dalawlem1  41194  dalawlem2  41195  dalawlem3  41196  dalawlem4  41197  dalawlem5  41198  dalawlem6  41199  dalawlem7  41200  dalawlem8  41201  dalawlem9  41202  dalawlem11  41204  dalawlem12  41205  dalawlem15  41208  pclfinclN  41273  poml4N  41276  osumcllem5N  41283  osumcllem7N  41285  pexmidlem2N  41294  pexmidlem4N  41296  pl42lem1N  41302  pl42lem2N  41303  pl42lem4N  41305  pl42N  41306  lhp2lt  41324  lhpexle2lem  41332  lhpexle3lem  41334  lhpj1  41345  lhpmcvr3  41348  lhpmcvr4N  41349  lhpmcvr5N  41350  lhpmcvr6N  41351  lhp2at0  41355  lhp2atnle  41356  lhpelim  41360  lhpmod2i2  41361  lhpmod6i1  41362  lhprelat3N  41363  lhple  41365  lhpat3  41369  4atexlemkl  41380  ltrnm  41454  ltrnj  41455  ltrnel  41462  ltrncnvel  41465  trljat1  41489  trljat2  41490  trlval3  41510  arglem1N  41513  cdlemc1  41514  cdlemc2  41515  cdlemc4  41517  cdlemc5  41518  cdlemc6  41519  cdlemd2  41522  cdlemd3  41523  cdlemd4  41524  cdlemd7  41527  cdleme0aa  41533  cdleme0b  41535  cdleme0c  41536  cdleme0e  41540  cdleme0fN  41541  cdlemeulpq  41543  cdleme01N  41544  cdleme0ex1N  41546  cdleme3g  41557  cdleme3h  41558  cdleme3  41560  cdleme4a  41562  cdleme5  41563  cdleme7aa  41565  cdleme7c  41568  cdleme7d  41569  cdleme7e  41570  cdleme7ga  41571  cdleme7  41572  cdleme8  41573  cdleme9  41576  cdleme10  41577  cdleme11c  41584  cdleme11e  41586  cdleme11fN  41587  cdleme11g  41588  cdleme11k  41591  cdleme11  41593  cdleme13  41595  cdleme15b  41598  cdleme15d  41600  cdleme15  41601  cdleme16b  41602  cdleme16e  41605  cdleme16f  41606  cdleme17b  41610  cdleme17c  41611  cdleme22gb  41617  cdlemednpq  41622  cdleme19b  41627  cdleme19c  41628  cdleme19e  41630  cdleme20aN  41632  cdleme20bN  41633  cdleme20c  41634  cdleme20d  41635  cdleme20e  41636  cdleme20j  41641  cdleme20k  41642  cdleme20l2  41644  cdleme20l  41645  cdleme20m  41646  cdleme21c  41650  cdleme21ct  41652  cdleme22aa  41662  cdleme22b  41664  cdleme22cN  41665  cdleme22d  41666  cdleme22e  41667  cdleme22eALTN  41668  cdleme22f  41669  cdleme22g  41671  cdleme23a  41672  cdleme23b  41673  cdleme23c  41674  cdleme27N  41692  cdleme28a  41693  cdleme28b  41694  cdleme29ex  41697  cdleme30a  41701  cdlemefr29exN  41725  cdleme32b  41765  cdleme32c  41766  cdleme32e  41768  cdleme35a  41771  cdleme35fnpq  41772  cdleme35b  41773  cdleme35c  41774  cdleme35d  41775  cdleme35f  41777  cdleme42c  41795  cdleme42e  41802  cdleme42h  41805  cdleme42i  41806  cdleme42mgN  41811  cdleme48bw  41825  cdlemeg46frv  41848  cdlemeg46vrg  41850  cdlemeg46rgv  41851  cdlemeg46req  41852  cdleme50eq  41864  cdlemf1  41884  trlord  41892  cdlemg2fv2  41923  cdlemg2m  41927  cdlemg7fvbwN  41930  cdlemg4c  41935  cdlemg4  41940  cdlemg6c  41943  cdlemg8b  41951  cdlemg10bALTN  41959  cdlemg10c  41962  cdlemg10  41964  cdlemg11b  41965  cdlemg12f  41971  cdlemg12g  41972  cdlemg12  41973  cdlemg13a  41974  cdlemg17a  41984  cdlemg17dALTN  41987  cdlemg17  42000  cdlemg18b  42002  cdlemg19a  42006  cdlemg19  42007  cdlemg27a  42015  cdlemg27b  42019  cdlemg31a  42020  cdlemg31b  42021  cdlemg33b0  42024  cdlemg33a  42029  cdlemg35  42036  trlcolem  42049  cdlemg42  42052  cdlemg44a  42054  cdlemg46  42058  trljco  42063  trljco2  42064  tendococl  42095  tendopltp  42103  cdlemh1  42138  cdlemh2  42139  cdlemi1  42141  cdlemi  42143  cdlemk3  42156  cdlemk4  42157  cdlemkvcl  42165  cdlemk10  42166  cdlemk7  42171  cdlemk11  42172  cdlemk12  42173  cdlemkole  42176  cdlemk14  42177  cdlemk15  42178  cdlemk1u  42182  cdlemk5u  42184  cdlemk7u  42193  cdlemk11u  42194  cdlemk12u  42195  cdlemk37  42237  cdlemk39  42239  cdlemkid1  42245  cdlemkid2  42247  cdlemk48  42273  cdlemk50  42275  cdlemk51  42276  cdlemk52  42277  cdlemk39u  42291  dia11N  42371  dia2dimlem1  42387  dia2dimlem2  42388  dia2dimlem3  42389  dia2dimlem10  42396  dia2dimlem12  42398  cdlemm10N  42441  dib11N  42483  diblss  42493  cdlemn2  42518  cdlemn10  42529  dihjustlem  42539  dihord1  42541  dihord2a  42542  dihord2b  42543  dihord2cN  42544  dihord11b  42545  dihord11c  42547  dihord2pre  42548  dihord2pre2  42549  dib2dim  42566  dih2dimb  42567  dihvalcq2  42570  dihopelvalcpre  42571  dihord6apre  42579  dihord5b  42582  dihord6b  42583  dihord5apre  42585  dih11  42588  dihwN  42612  dihmeetlem1N  42613  dihglblem5apreN  42614  dihglblem2N  42617  dihglblem3N  42618  dihmeetlem2N  42622  dihglbcpreN  42623  dihmeetbclemN  42627  dihmeetlem3N  42628  dihmeetlem4preN  42629  dihmeetlem6  42632  dihmeetlem7N  42633  dihjatc1  42634  dihjatc2N  42635  dihjatc3  42636  dihmeetlem9N  42638  dihmeetlem10N  42639  dihmeetlem11N  42640  dihmeetlem15N  42644  dihmeetlem16N  42645  dihmeetlem17N  42646  dihmeetlem19N  42648  dihmeetlem20N  42649  dihmeetALTN  42650  dihmeet2  42669  djhljjN  42725  djhj  42727  dihjatcclem1  42741  dihjatcclem2  42742  dihjatcclem4  42744  dihprrnlem1N  42747  dihprrnlem2  42748  dihjat6  42757  dihjat5N  42760  dvh4dimat  42761