Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hllatd Structured version   Visualization version   GIF version

Theorem hllatd 36382
Description: Deduction form of hllat 36381. 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
StepHypRef Expression
1 hllatd.1 . 2 (𝜑𝐾 ∈ HL)
2 hllat 36381 . 2 (𝐾 ∈ HL → 𝐾 ∈ Lat)
31, 2syl 17 1 (𝜑𝐾 ∈ Lat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Latclat 17645  HLchlt 36368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-dm 5559  df-iota 6308  df-fv 6357  df-ov 7148  df-atl 36316  df-cvlat 36340  df-hlat 36369
This theorem is referenced by:  hlrelat  36420  hlrelat2  36421  exatleN  36422  intnatN  36425  hlrelat3  36430  cvrval3  36431  cvrexchlem  36437  lnnat  36445  2atlt  36457  atexchcvrN  36458  atbtwn  36464  4noncolr3  36471  athgt  36474  3dim0  36475  3dimlem3a  36478  3dimlem4a  36481  3dim3  36487  1cvratex  36491  1cvrjat  36493  hlatexch4  36499  ps-2b  36500  3atlem1  36501  3atlem2  36502  3atlem4  36504  3atlem5  36505  3atlem6  36506  2llnmat  36542  2at0mat0  36543  2atm  36545  ps-2c  36546  llnmlplnN  36557  lplnle  36558  2atmat  36579  lplnexllnN  36582  2llnjaN  36584  lvoli3  36595  lvoli2  36599  lvolnle3at  36600  islvol2aN  36610  4atlem3  36614  4atlem3a  36615  4atlem3b  36616  4atlem4a  36617  4atlem4b  36618  4atlem4c  36619  4atlem4d  36620  4atlem9  36621  4atlem10a  36622  4atlem10  36624  4atlem11a  36625  4atlem11b  36626  4atlem11  36627  4atlem12a  36628  4atlem12b  36629  4atlem12  36630  4at  36631  4at2  36632  lplncvrlvol2  36633  lplncvrlvol  36634  2lplnja  36637  dalemkelat  36642  lneq2at  36796  lncmp  36801  2lnat  36802  cdlema1N  36809  cdlemblem  36811  cdlemb  36812  paddasslem2  36839  paddasslem5  36842  paddasslem8  36845  paddasslem12  36849  paddasslem13  36850  paddasslem15  36852  pmodlem1  36864  pmodlem2  36865  atmod1i1m  36876  llnmod1i2  36878  llnmod2i2  36881  llnexchb2lem  36886  llnexchb2  36887  dalawlem1  36889  dalawlem2  36890  dalawlem3  36891  dalawlem4  36892  dalawlem5  36893  dalawlem6  36894  dalawlem7  36895  dalawlem8  36896  dalawlem9  36897  dalawlem11  36899  dalawlem12  36900  dalawlem15  36903  pclfinclN  36968  poml4N  36971  osumcllem5N  36978  osumcllem7N  36980  pexmidlem2N  36989  pexmidlem4N  36991  pl42lem1N  36997  pl42lem2N  36998  pl42lem4N  37000  pl42N  37001  lhp2lt  37019  lhpexle2lem  37027  lhpexle3lem  37029  lhpj1  37040  lhpmcvr3  37043  lhpmcvr4N  37044  lhpmcvr5N  37045  lhpmcvr6N  37046  lhp2at0  37050  lhp2atnle  37051  lhpelim  37055  lhpmod2i2  37056  lhpmod6i1  37057  lhprelat3N  37058  lhple  37060  lhpat3  37064  4atexlemkl  37075  ltrnm  37149  ltrnj  37150  ltrnel  37157  ltrncnvel  37160  trljat1  37184  trljat2  37185  trlval3  37205  arglem1N  37208  cdlemc1  37209  cdlemc2  37210  cdlemc4  37212  cdlemc5  37213  cdlemc6  37214  cdlemd2  37217  cdlemd3  37218  cdlemd4  37219  cdlemd7  37222  cdleme0aa  37228  cdleme0b  37230  cdleme0c  37231  cdleme0e  37235  cdleme0fN  37236  cdlemeulpq  37238  cdleme01N  37239  cdleme0ex1N  37241  cdleme3g  37252  cdleme3h  37253  cdleme3  37255  cdleme4a  37257  cdleme5  37258  cdleme7aa  37260  cdleme7c  37263  cdleme7d  37264  cdleme7e  37265  cdleme7ga  37266  cdleme7  37267  cdleme8  37268  cdleme9  37271  cdleme10  37272  cdleme11c  37279  cdleme11e  37281  cdleme11fN  37282  cdleme11g  37283  cdleme11k  37286  cdleme11  37288  cdleme13  37290  cdleme15b  37293  cdleme15d  37295  cdleme15  37296  cdleme16b  37297  cdleme16e  37300  cdleme16f  37301  cdleme17b  37305  cdleme17c  37306  cdleme22gb  37312  cdlemednpq  37317  cdleme19b  37322  cdleme19c  37323  cdleme19e  37325  cdleme20aN  37327  cdleme20bN  37328  cdleme20c  37329  cdleme20d  37330  cdleme20e  37331  cdleme20j  37336  cdleme20k  37337  cdleme20l2  37339  cdleme20l  37340  cdleme20m  37341  cdleme21c  37345  cdleme21ct  37347  cdleme22aa  37357  cdleme22b  37359  cdleme22cN  37360  cdleme22d  37361  cdleme22e  37362  cdleme22eALTN  37363  cdleme22f  37364  cdleme22g  37366  cdleme23a  37367  cdleme23b  37368  cdleme23c  37369  cdleme27N  37387  cdleme28a  37388  cdleme28b  37389  cdleme29ex  37392  cdleme30a  37396  cdlemefr29exN  37420  cdleme32b  37460  cdleme32c  37461  cdleme32e  37463  cdleme35a  37466  cdleme35fnpq  37467  cdleme35b  37468  cdleme35c  37469  cdleme35d  37470  cdleme35f  37472  cdleme42c  37490  cdleme42e  37497  cdleme42h  37500  cdleme42i  37501  cdleme42mgN  37506  cdleme48bw  37520  cdlemeg46frv  37543  cdlemeg46vrg  37545  cdlemeg46rgv  37546  cdlemeg46req  37547  cdleme50eq  37559  cdlemf1  37579  trlord  37587  cdlemg2fv2  37618  cdlemg2m  37622  cdlemg7fvbwN  37625  cdlemg4c  37630  cdlemg4  37635  cdlemg6c  37638  cdlemg8b  37646  cdlemg10bALTN  37654  cdlemg10c  37657  cdlemg10  37659  cdlemg11b  37660  cdlemg12f  37666  cdlemg12g  37667  cdlemg12  37668  cdlemg13a  37669  cdlemg17a  37679  cdlemg17dALTN  37682  cdlemg17  37695  cdlemg18b  37697  cdlemg19a  37701  cdlemg19  37702  cdlemg27a  37710  cdlemg27b  37714  cdlemg31a  37715  cdlemg31b  37716  cdlemg33b0  37719  cdlemg33a  37724  cdlemg35  37731  trlcolem  37744  cdlemg42  37747  cdlemg44a  37749  cdlemg46  37753  trljco  37758  trljco2  37759  tendococl  37790  tendopltp  37798  cdlemh1  37833  cdlemh2  37834  cdlemi1  37836  cdlemi  37838  cdlemk3  37851  cdlemk4  37852  cdlemkvcl  37860  cdlemk10  37861  cdlemk7  37866  cdlemk11  37867  cdlemk12  37868  cdlemkole  37871  cdlemk14  37872  cdlemk15  37873  cdlemk1u  37877  cdlemk5u  37879  cdlemk7u  37888  cdlemk11u  37889  cdlemk12u  37890  cdlemk37  37932  cdlemk39  37934  cdlemkid1  37940  cdlemkid2  37942  cdlemk48  37968  cdlemk50  37970  cdlemk51  37971  cdlemk52  37972  cdlemk39u  37986  dia11N  38066  dia2dimlem1  38082  dia2dimlem2  38083  dia2dimlem3  38084  dia2dimlem10  38091  dia2dimlem12  38093  cdlemm10N  38136  dib11N  38178  diblss  38188  cdlemn2  38213  cdlemn10  38224  dihjustlem  38234  dihord1  38236  dihord2a  38237  dihord2b  38238  dihord2cN  38239  dihord11b  38240  dihord11c  38242  dihord2pre  38243  dihord2pre2  38244  dib2dim  38261  dih2dimb  38262  dihvalcq2  38265  dihopelvalcpre  38266  dihord6apre  38274  dihord5b  38277  dihord6b  38278  dihord5apre  38280  dih11  38283  dihwN  38307  dihmeetlem1N  38308  dihglblem5apreN  38309  dihglblem2N  38312  dihglblem3N  38313  dihmeetlem2N  38317  dihglbcpreN  38318  dihmeetbclemN  38322  dihmeetlem3N  38323  dihmeetlem4preN  38324  dihmeetlem6  38327  dihmeetlem7N  38328  dihjatc1  38329  dihjatc2N  38330  dihjatc3  38331  dihmeetlem9N  38333  dihmeetlem10N  38334  dihmeetlem11N  38335  dihmeetlem15N  38339  dihmeetlem16N  38340  dihmeetlem17N  38341  dihmeetlem19N  38343  dihmeetlem20N  38344  dihmeetALTN  38345  dihmeet2  38364  djhljjN  38420  djhj  38422  dihjatcclem1  38436  dihjatcclem2  38437  dihjatcclem4  38439  dihprrnlem1N  38442  dihprrnlem2  38443  dihjat6  38452  dihjat5N  38455  dvh4dimat  38456
  Copyright terms: Public domain W3C validator