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 37872
Description: Deduction form of hllat 37871. 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 37871 . 2 (𝐾 ∈ HL → 𝐾 ∈ Lat)
31, 2syl 17 1 (𝜑𝐾 ∈ Lat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Latclat 18325  HLchlt 37858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-dm 5644  df-iota 6449  df-fv 6505  df-ov 7361  df-atl 37806  df-cvlat 37830  df-hlat 37859
This theorem is referenced by:  hlrelat  37911  hlrelat2  37912  exatleN  37913  intnatN  37916  hlrelat3  37921  cvrval3  37922  cvrexchlem  37928  lnnat  37936  2atlt  37948  atexchcvrN  37949  atbtwn  37955  4noncolr3  37962  athgt  37965  3dim0  37966  3dimlem3a  37969  3dimlem4a  37972  3dim3  37978  1cvratex  37982  1cvrjat  37984  hlatexch4  37990  ps-2b  37991  3atlem1  37992  3atlem2  37993  3atlem4  37995  3atlem5  37996  3atlem6  37997  2llnmat  38033  2at0mat0  38034  2atm  38036  ps-2c  38037  llnmlplnN  38048  lplnle  38049  2atmat  38070  lplnexllnN  38073  2llnjaN  38075  lvoli3  38086  lvoli2  38090  lvolnle3at  38091  islvol2aN  38101  4atlem3  38105  4atlem3a  38106  4atlem3b  38107  4atlem4a  38108  4atlem4b  38109  4atlem4c  38110  4atlem4d  38111  4atlem9  38112  4atlem10a  38113  4atlem10  38115  4atlem11a  38116  4atlem11b  38117  4atlem11  38118  4atlem12a  38119  4atlem12b  38120  4atlem12  38121  4at  38122  4at2  38123  lplncvrlvol2  38124  lplncvrlvol  38125  2lplnja  38128  dalemkelat  38133  lneq2at  38287  lncmp  38292  2lnat  38293  cdlema1N  38300  cdlemblem  38302  cdlemb  38303  paddasslem2  38330  paddasslem5  38333  paddasslem8  38336  paddasslem12  38340  paddasslem13  38341  paddasslem15  38343  pmodlem1  38355  pmodlem2  38356  atmod1i1m  38367  llnmod1i2  38369  llnmod2i2  38372  llnexchb2lem  38377  llnexchb2  38378  dalawlem1  38380  dalawlem2  38381  dalawlem3  38382  dalawlem4  38383  dalawlem5  38384  dalawlem6  38385  dalawlem7  38386  dalawlem8  38387  dalawlem9  38388  dalawlem11  38390  dalawlem12  38391  dalawlem15  38394  pclfinclN  38459  poml4N  38462  osumcllem5N  38469  osumcllem7N  38471  pexmidlem2N  38480  pexmidlem4N  38482  pl42lem1N  38488  pl42lem2N  38489  pl42lem4N  38491  pl42N  38492  lhp2lt  38510  lhpexle2lem  38518  lhpexle3lem  38520  lhpj1  38531  lhpmcvr3  38534  lhpmcvr4N  38535  lhpmcvr5N  38536  lhpmcvr6N  38537  lhp2at0  38541  lhp2atnle  38542  lhpelim  38546  lhpmod2i2  38547  lhpmod6i1  38548  lhprelat3N  38549  lhple  38551  lhpat3  38555  4atexlemkl  38566  ltrnm  38640  ltrnj  38641  ltrnel  38648  ltrncnvel  38651  trljat1  38675  trljat2  38676  trlval3  38696  arglem1N  38699  cdlemc1  38700  cdlemc2  38701  cdlemc4  38703  cdlemc5  38704  cdlemc6  38705  cdlemd2  38708  cdlemd3  38709  cdlemd4  38710  cdlemd7  38713  cdleme0aa  38719  cdleme0b  38721  cdleme0c  38722  cdleme0e  38726  cdleme0fN  38727  cdlemeulpq  38729  cdleme01N  38730  cdleme0ex1N  38732  cdleme3g  38743  cdleme3h  38744  cdleme3  38746  cdleme4a  38748  cdleme5  38749  cdleme7aa  38751  cdleme7c  38754  cdleme7d  38755  cdleme7e  38756  cdleme7ga  38757  cdleme7  38758  cdleme8  38759  cdleme9  38762  cdleme10  38763  cdleme11c  38770  cdleme11e  38772  cdleme11fN  38773  cdleme11g  38774  cdleme11k  38777  cdleme11  38779  cdleme13  38781  cdleme15b  38784  cdleme15d  38786  cdleme15  38787  cdleme16b  38788  cdleme16e  38791  cdleme16f  38792  cdleme17b  38796  cdleme17c  38797  cdleme22gb  38803  cdlemednpq  38808  cdleme19b  38813  cdleme19c  38814  cdleme19e  38816  cdleme20aN  38818  cdleme20bN  38819  cdleme20c  38820  cdleme20d  38821  cdleme20e  38822  cdleme20j  38827  cdleme20k  38828  cdleme20l2  38830  cdleme20l  38831  cdleme20m  38832  cdleme21c  38836  cdleme21ct  38838  cdleme22aa  38848  cdleme22b  38850  cdleme22cN  38851  cdleme22d  38852  cdleme22e  38853  cdleme22eALTN  38854  cdleme22f  38855  cdleme22g  38857  cdleme23a  38858  cdleme23b  38859  cdleme23c  38860  cdleme27N  38878  cdleme28a  38879  cdleme28b  38880  cdleme29ex  38883  cdleme30a  38887  cdlemefr29exN  38911  cdleme32b  38951  cdleme32c  38952  cdleme32e  38954  cdleme35a  38957  cdleme35fnpq  38958  cdleme35b  38959  cdleme35c  38960  cdleme35d  38961  cdleme35f  38963  cdleme42c  38981  cdleme42e  38988  cdleme42h  38991  cdleme42i  38992  cdleme42mgN  38997  cdleme48bw  39011  cdlemeg46frv  39034  cdlemeg46vrg  39036  cdlemeg46rgv  39037  cdlemeg46req  39038  cdleme50eq  39050  cdlemf1  39070  trlord  39078  cdlemg2fv2  39109  cdlemg2m  39113  cdlemg7fvbwN  39116  cdlemg4c  39121  cdlemg4  39126  cdlemg6c  39129  cdlemg8b  39137  cdlemg10bALTN  39145  cdlemg10c  39148  cdlemg10  39150  cdlemg11b  39151  cdlemg12f  39157  cdlemg12g  39158  cdlemg12  39159  cdlemg13a  39160  cdlemg17a  39170  cdlemg17dALTN  39173  cdlemg17  39186  cdlemg18b  39188  cdlemg19a  39192  cdlemg19  39193  cdlemg27a  39201  cdlemg27b  39205  cdlemg31a  39206  cdlemg31b  39207  cdlemg33b0  39210  cdlemg33a  39215  cdlemg35  39222  trlcolem  39235  cdlemg42  39238  cdlemg44a  39240  cdlemg46  39244  trljco  39249  trljco2  39250  tendococl  39281  tendopltp  39289  cdlemh1  39324  cdlemh2  39325  cdlemi1  39327  cdlemi  39329  cdlemk3  39342  cdlemk4  39343  cdlemkvcl  39351  cdlemk10  39352  cdlemk7  39357  cdlemk11  39358  cdlemk12  39359  cdlemkole  39362  cdlemk14  39363  cdlemk15  39364  cdlemk1u  39368  cdlemk5u  39370  cdlemk7u  39379  cdlemk11u  39380  cdlemk12u  39381  cdlemk37  39423  cdlemk39  39425  cdlemkid1  39431  cdlemkid2  39433  cdlemk48  39459  cdlemk50  39461  cdlemk51  39462  cdlemk52  39463  cdlemk39u  39477  dia11N  39557  dia2dimlem1  39573  dia2dimlem2  39574  dia2dimlem3  39575  dia2dimlem10  39582  dia2dimlem12  39584  cdlemm10N  39627  dib11N  39669  diblss  39679  cdlemn2  39704  cdlemn10  39715  dihjustlem  39725  dihord1  39727  dihord2a  39728  dihord2b  39729  dihord2cN  39730  dihord11b  39731  dihord11c  39733  dihord2pre  39734  dihord2pre2  39735  dib2dim  39752  dih2dimb  39753  dihvalcq2  39756  dihopelvalcpre  39757  dihord6apre  39765  dihord5b  39768  dihord6b  39769  dihord5apre  39771  dih11  39774  dihwN  39798  dihmeetlem1N  39799  dihglblem5apreN  39800  dihglblem2N  39803  dihglblem3N  39804  dihmeetlem2N  39808  dihglbcpreN  39809  dihmeetbclemN  39813  dihmeetlem3N  39814  dihmeetlem4preN  39815  dihmeetlem6  39818  dihmeetlem7N  39819  dihjatc1  39820  dihjatc2N  39821  dihjatc3  39822  dihmeetlem9N  39824  dihmeetlem10N  39825  dihmeetlem11N  39826  dihmeetlem15N  39830  dihmeetlem16N  39831  dihmeetlem17N  39832  dihmeetlem19N  39834  dihmeetlem20N  39835  dihmeetALTN  39836  dihmeet2  39855  djhljjN  39911  djhj  39913  dihjatcclem1  39927  dihjatcclem2  39928  dihjatcclem4  39930  dihprrnlem1N  39933  dihprrnlem2  39934  dihjat6  39943  dihjat5N  39946  dvh4dimat  39947
  Copyright terms: Public domain W3C validator