Theorem hllatd 40421

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Latclat 18605  HLchlt 40407

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5661  df-iota 6494  df-fv 6546  df-ov 7423  df-atl 40355  df-cvlat 40379  df-hlat 40408

This theorem is used by:  hlrelat  40459  hlrelat2  40460  exatleN  40461  intnatN  40464  hlrelat3  40469  cvrval3  40470  cvrexchlem  40476  lnnat  40484  2atlt  40496  atexchcvrN  40497  atbtwn  40503  4noncolr3  40510  athgt  40513  3dim0  40514  3dimlem3a  40517  3dimlem4a  40520  3dim3  40526  1cvratex  40530  1cvrjat  40532  hlatexch4  40538  ps-2b  40539  3atlem1  40540  3atlem2  40541  3atlem4  40543  3atlem5  40544  3atlem6  40545  2llnmat  40581  2at0mat0  40582  2atm  40584  ps-2c  40585  llnmlplnN  40596  lplnle  40597  2atmat  40618  lplnexllnN  40621  2llnjaN  40623  lvoli3  40634  lvoli2  40638  lvolnle3at  40639  islvol2aN  40649  4atlem3  40653  4atlem3a  40654  4atlem3b  40655  4atlem4a  40656  4atlem4b  40657  4atlem4c  40658  4atlem4d  40659  4atlem9  40660  4atlem10a  40661  4atlem10  40663  4atlem11a  40664  4atlem11b  40665  4atlem11  40666  4atlem12a  40667  4atlem12b  40668  4atlem12  40669  4at  40670  4at2  40671  lplncvrlvol2  40672  lplncvrlvol  40673  2lplnja  40676  dalemkelat  40681  lneq2at  40835  lncmp  40840  2lnat  40841  cdlema1N  40848  cdlemblem  40850  cdlemb  40851  paddasslem2  40878  paddasslem5  40881  paddasslem8  40884  paddasslem12  40888  paddasslem13  40889  paddasslem15  40891  pmodlem1  40903  pmodlem2  40904  atmod1i1m  40915  llnmod1i2  40917  llnmod2i2  40920  llnexchb2lem  40925  llnexchb2  40926  dalawlem1  40928  dalawlem2  40929  dalawlem3  40930  dalawlem4  40931  dalawlem5  40932  dalawlem6  40933  dalawlem7  40934  dalawlem8  40935  dalawlem9  40936  dalawlem11  40938  dalawlem12  40939  dalawlem15  40942  pclfinclN  41007  poml4N  41010  osumcllem5N  41017  osumcllem7N  41019  pexmidlem2N  41028  pexmidlem4N  41030  pl42lem1N  41036  pl42lem2N  41037  pl42lem4N  41039  pl42N  41040  lhp2lt  41058  lhpexle2lem  41066  lhpexle3lem  41068  lhpj1  41079  lhpmcvr3  41082  lhpmcvr4N  41083  lhpmcvr5N  41084  lhpmcvr6N  41085  lhp2at0  41089  lhp2atnle  41090  lhpelim  41094  lhpmod2i2  41095  lhpmod6i1  41096  lhprelat3N  41097  lhple  41099  lhpat3  41103  4atexlemkl  41114  ltrnm  41188  ltrnj  41189  ltrnel  41196  ltrncnvel  41199  trljat1  41223  trljat2  41224  trlval3  41244  arglem1N  41247  cdlemc1  41248  cdlemc2  41249  cdlemc4  41251  cdlemc5  41252  cdlemc6  41253  cdlemd2  41256  cdlemd3  41257  cdlemd4  41258  cdlemd7  41261  cdleme0aa  41267  cdleme0b  41269  cdleme0c  41270  cdleme0e  41274  cdleme0fN  41275  cdlemeulpq  41277  cdleme01N  41278  cdleme0ex1N  41280  cdleme3g  41291  cdleme3h  41292  cdleme3  41294  cdleme4a  41296  cdleme5  41297  cdleme7aa  41299  cdleme7c  41302  cdleme7d  41303  cdleme7e  41304  cdleme7ga  41305  cdleme7  41306  cdleme8  41307  cdleme9  41310  cdleme10  41311  cdleme11c  41318  cdleme11e  41320  cdleme11fN  41321  cdleme11g  41322  cdleme11k  41325  cdleme11  41327  cdleme13  41329  cdleme15b  41332  cdleme15d  41334  cdleme15  41335  cdleme16b  41336  cdleme16e  41339  cdleme16f  41340  cdleme17b  41344  cdleme17c  41345  cdleme22gb  41351  cdlemednpq  41356  cdleme19b  41361  cdleme19c  41362  cdleme19e  41364  cdleme20aN  41366  cdleme20bN  41367  cdleme20c  41368  cdleme20d  41369  cdleme20e  41370  cdleme20j  41375  cdleme20k  41376  cdleme20l2  41378  cdleme20l  41379  cdleme20m  41380  cdleme21c  41384  cdleme21ct  41386  cdleme22aa  41396  cdleme22b  41398  cdleme22cN  41399  cdleme22d  41400  cdleme22e  41401  cdleme22eALTN  41402  cdleme22f  41403  cdleme22g  41405  cdleme23a  41406  cdleme23b  41407  cdleme23c  41408  cdleme27N  41426  cdleme28a  41427  cdleme28b  41428  cdleme29ex  41431  cdleme30a  41435  cdlemefr29exN  41459  cdleme32b  41499  cdleme32c  41500  cdleme32e  41502  cdleme35a  41505  cdleme35fnpq  41506  cdleme35b  41507  cdleme35c  41508  cdleme35d  41509  cdleme35f  41511  cdleme42c  41529  cdleme42e  41536  cdleme42h  41539  cdleme42i  41540  cdleme42mgN  41545  cdleme48bw  41559  cdlemeg46frv  41582  cdlemeg46vrg  41584  cdlemeg46rgv  41585  cdlemeg46req  41586  cdleme50eq  41598  cdlemf1  41618  trlord  41626  cdlemg2fv2  41657  cdlemg2m  41661  cdlemg7fvbwN  41664  cdlemg4c  41669  cdlemg4  41674  cdlemg6c  41677  cdlemg8b  41685  cdlemg10bALTN  41693  cdlemg10c  41696  cdlemg10  41698  cdlemg11b  41699  cdlemg12f  41705  cdlemg12g  41706  cdlemg12  41707  cdlemg13a  41708  cdlemg17a  41718  cdlemg17dALTN  41721  cdlemg17  41734  cdlemg18b  41736  cdlemg19a  41740  cdlemg19  41741  cdlemg27a  41749  cdlemg27b  41753  cdlemg31a  41754  cdlemg31b  41755  cdlemg33b0  41758  cdlemg33a  41763  cdlemg35  41770  trlcolem  41783  cdlemg42  41786  cdlemg44a  41788  cdlemg46  41792  trljco  41797  trljco2  41798  tendococl  41829  tendopltp  41837  cdlemh1  41872  cdlemh2  41873  cdlemi1  41875  cdlemi  41877  cdlemk3  41890  cdlemk4  41891  cdlemkvcl  41899  cdlemk10  41900  cdlemk7  41905  cdlemk11  41906  cdlemk12  41907  cdlemkole  41910  cdlemk14  41911  cdlemk15  41912  cdlemk1u  41916  cdlemk5u  41918  cdlemk7u  41927  cdlemk11u  41928  cdlemk12u  41929  cdlemk37  41971  cdlemk39  41973  cdlemkid1  41979  cdlemkid2  41981  cdlemk48  42007  cdlemk50  42009  cdlemk51  42010  cdlemk52  42011  cdlemk39u  42025  dia11N  42105  dia2dimlem1  42121  dia2dimlem2  42122  dia2dimlem3  42123  dia2dimlem10  42130  dia2dimlem12  42132  cdlemm10N  42175  dib11N  42217  diblss  42227  cdlemn2  42252  cdlemn10  42263  dihjustlem  42273  dihord1  42275  dihord2a  42276  dihord2b  42277  dihord2cN  42278  dihord11b  42279  dihord11c  42281  dihord2pre  42282  dihord2pre2  42283  dib2dim  42300  dih2dimb  42301  dihvalcq2  42304  dihopelvalcpre  42305  dihord6apre  42313  dihord5b  42316  dihord6b  42317  dihord5apre  42319  dih11  42322  dihwN  42346  dihmeetlem1N  42347  dihglblem5apreN  42348  dihglblem2N  42351  dihglblem3N  42352  dihmeetlem2N  42356  dihglbcpreN  42357  dihmeetbclemN  42361  dihmeetlem3N  42362  dihmeetlem4preN  42363  dihmeetlem6  42366  dihmeetlem7N  42367  dihjatc1  42368  dihjatc2N  42369  dihjatc3  42370  dihmeetlem9N  42372  dihmeetlem10N  42373  dihmeetlem11N  42374  dihmeetlem15N  42378  dihmeetlem16N  42379  dihmeetlem17N  42380  dihmeetlem19N  42382  dihmeetlem20N  42383  dihmeetALTN  42384  dihmeet2  42403  djhljjN  42459  djhj  42461  dihjatcclem1  42475  dihjatcclem2  42476  dihjatcclem4  42478  dihprrnlem1N  42481  dihprrnlem2  42482  dihjat6  42491  dihjat5N  42494  dvh4dimat  42495