Theorem hllatd 40561

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Latclat 18617  HLchlt 40547

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-dm 5664  df-iota 6500  df-fv 6554  df-ov 7430  df-atl 40495  df-cvlat 40519  df-hlat 40548

This theorem is used by:  hlrelat  40599  hlrelat2  40600  exatleN  40601  intnatN  40604  hlrelat3  40609  cvrval3  40610  cvrexchlem  40616  lnnat  40624  2atlt  40636  atexchcvrN  40637  atbtwn  40643  4noncolr3  40650  athgt  40653  3dim0  40654  3dimlem3a  40657  3dimlem4a  40660  3dim3  40666  1cvratex  40670  1cvrjat  40672  hlatexch4  40678  ps-2b  40679  3atlem1  40680  3atlem2  40681  3atlem4  40683  3atlem5  40684  3atlem6  40685  2llnmat  40721  2at0mat0  40722  2atm  40724  ps-2c  40725  llnmlplnN  40736  lplnle  40737  2atmat  40758  lplnexllnN  40761  2llnjaN  40763  lvoli3  40774  lvoli2  40778  lvolnle3at  40779  islvol2aN  40789  4atlem3  40793  4atlem3a  40794  4atlem3b  40795  4atlem4a  40796  4atlem4b  40797  4atlem4c  40798  4atlem4d  40799  4atlem9  40800  4atlem10a  40801  4atlem10  40803  4atlem11a  40804  4atlem11b  40805  4atlem11  40806  4atlem12a  40807  4atlem12b  40808  4atlem12  40809  4at  40810  4at2  40811  lplncvrlvol2  40812  lplncvrlvol  40813  2lplnja  40816  dalemkelat  40821  lneq2at  40975  lncmp  40980  2lnat  40981  cdlema1N  40988  cdlemblem  40990  cdlemb  40991  paddasslem2  41018  paddasslem5  41021  paddasslem8  41024  paddasslem12  41028  paddasslem13  41029  paddasslem15  41031  pmodlem1  41043  pmodlem2  41044  atmod1i1m  41055  llnmod1i2  41057  llnmod2i2  41060  llnexchb2lem  41065  llnexchb2  41066  dalawlem1  41068  dalawlem2  41069  dalawlem3  41070  dalawlem4  41071  dalawlem5  41072  dalawlem6  41073  dalawlem7  41074  dalawlem8  41075  dalawlem9  41076  dalawlem11  41078  dalawlem12  41079  dalawlem15  41082  pclfinclN  41147  poml4N  41150  osumcllem5N  41157  osumcllem7N  41159  pexmidlem2N  41168  pexmidlem4N  41170  pl42lem1N  41176  pl42lem2N  41177  pl42lem4N  41179  pl42N  41180  lhp2lt  41198  lhpexle2lem  41206  lhpexle3lem  41208  lhpj1  41219  lhpmcvr3  41222  lhpmcvr4N  41223  lhpmcvr5N  41224  lhpmcvr6N  41225  lhp2at0  41229  lhp2atnle  41230  lhpelim  41234  lhpmod2i2  41235  lhpmod6i1  41236  lhprelat3N  41237  lhple  41239  lhpat3  41243  4atexlemkl  41254  ltrnm  41328  ltrnj  41329  ltrnel  41336  ltrncnvel  41339  trljat1  41363  trljat2  41364  trlval3  41384  arglem1N  41387  cdlemc1  41388  cdlemc2  41389  cdlemc4  41391  cdlemc5  41392  cdlemc6  41393  cdlemd2  41396  cdlemd3  41397  cdlemd4  41398  cdlemd7  41401  cdleme0aa  41407  cdleme0b  41409  cdleme0c  41410  cdleme0e  41414  cdleme0fN  41415  cdlemeulpq  41417  cdleme01N  41418  cdleme0ex1N  41420  cdleme3g  41431  cdleme3h  41432  cdleme3  41434  cdleme4a  41436  cdleme5  41437  cdleme7aa  41439  cdleme7c  41442  cdleme7d  41443  cdleme7e  41444  cdleme7ga  41445  cdleme7  41446  cdleme8  41447  cdleme9  41450  cdleme10  41451  cdleme11c  41458  cdleme11e  41460  cdleme11fN  41461  cdleme11g  41462  cdleme11k  41465  cdleme11  41467  cdleme13  41469  cdleme15b  41472  cdleme15d  41474  cdleme15  41475  cdleme16b  41476  cdleme16e  41479  cdleme16f  41480  cdleme17b  41484  cdleme17c  41485  cdleme22gb  41491  cdlemednpq  41496  cdleme19b  41501  cdleme19c  41502  cdleme19e  41504  cdleme20aN  41506  cdleme20bN  41507  cdleme20c  41508  cdleme20d  41509  cdleme20e  41510  cdleme20j  41515  cdleme20k  41516  cdleme20l2  41518  cdleme20l  41519  cdleme20m  41520  cdleme21c  41524  cdleme21ct  41526  cdleme22aa  41536  cdleme22b  41538  cdleme22cN  41539  cdleme22d  41540  cdleme22e  41541  cdleme22eALTN  41542  cdleme22f  41543  cdleme22g  41545  cdleme23a  41546  cdleme23b  41547  cdleme23c  41548  cdleme27N  41566  cdleme28a  41567  cdleme28b  41568  cdleme29ex  41571  cdleme30a  41575  cdlemefr29exN  41599  cdleme32b  41639  cdleme32c  41640  cdleme32e  41642  cdleme35a  41645  cdleme35fnpq  41646  cdleme35b  41647  cdleme35c  41648  cdleme35d  41649  cdleme35f  41651  cdleme42c  41669  cdleme42e  41676  cdleme42h  41679  cdleme42i  41680  cdleme42mgN  41685  cdleme48bw  41699  cdlemeg46frv  41722  cdlemeg46vrg  41724  cdlemeg46rgv  41725  cdlemeg46req  41726  cdleme50eq  41738  cdlemf1  41758  trlord  41766  cdlemg2fv2  41797  cdlemg2m  41801  cdlemg7fvbwN  41804  cdlemg4c  41809  cdlemg4  41814  cdlemg6c  41817  cdlemg8b  41825  cdlemg10bALTN  41833  cdlemg10c  41836  cdlemg10  41838  cdlemg11b  41839  cdlemg12f  41845  cdlemg12g  41846  cdlemg12  41847  cdlemg13a  41848  cdlemg17a  41858  cdlemg17dALTN  41861  cdlemg17  41874  cdlemg18b  41876  cdlemg19a  41880  cdlemg19  41881  cdlemg27a  41889  cdlemg27b  41893  cdlemg31a  41894  cdlemg31b  41895  cdlemg33b0  41898  cdlemg33a  41903  cdlemg35  41910  trlcolem  41923  cdlemg42  41926  cdlemg44a  41928  cdlemg46  41932  trljco  41937  trljco2  41938  tendococl  41969  tendopltp  41977  cdlemh1  42012  cdlemh2  42013  cdlemi1  42015  cdlemi  42017  cdlemk3  42030  cdlemk4  42031  cdlemkvcl  42039  cdlemk10  42040  cdlemk7  42045  cdlemk11  42046  cdlemk12  42047  cdlemkole  42050  cdlemk14  42051  cdlemk15  42052  cdlemk1u  42056  cdlemk5u  42058  cdlemk7u  42067  cdlemk11u  42068  cdlemk12u  42069  cdlemk37  42111  cdlemk39  42113  cdlemkid1  42119  cdlemkid2  42121  cdlemk48  42147  cdlemk50  42149  cdlemk51  42150  cdlemk52  42151  cdlemk39u  42165  dia11N  42245  dia2dimlem1  42261  dia2dimlem2  42262  dia2dimlem3  42263  dia2dimlem10  42270  dia2dimlem12  42272  cdlemm10N  42315  dib11N  42357  diblss  42367  cdlemn2  42392  cdlemn10  42403  dihjustlem  42413  dihord1  42415  dihord2a  42416  dihord2b  42417  dihord2cN  42418  dihord11b  42419  dihord11c  42421  dihord2pre  42422  dihord2pre2  42423  dib2dim  42440  dih2dimb  42441  dihvalcq2  42444  dihopelvalcpre  42445  dihord6apre  42453  dihord5b  42456  dihord6b  42457  dihord5apre  42459  dih11  42462  dihwN  42486  dihmeetlem1N  42487  dihglblem5apreN  42488  dihglblem2N  42491  dihglblem3N  42492  dihmeetlem2N  42496  dihglbcpreN  42497  dihmeetbclemN  42501  dihmeetlem3N  42502  dihmeetlem4preN  42503  dihmeetlem6  42506  dihmeetlem7N  42507  dihjatc1  42508  dihjatc2N  42509  dihjatc3  42510  dihmeetlem9N  42512  dihmeetlem10N  42513  dihmeetlem11N  42514  dihmeetlem15N  42518  dihmeetlem16N  42519  dihmeetlem17N  42520  dihmeetlem19N  42522  dihmeetlem20N  42523  dihmeetALTN  42524  dihmeet2  42543  djhljjN  42599  djhj  42601  dihjatcclem1  42615  dihjatcclem2  42616  dihjatcclem4  42618  dihprrnlem1N  42621  dihprrnlem2  42622  dihjat6  42631  dihjat5N  42634  dvh4dimat  42635