Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvlatl Structured version   Unicode version

Theorem cvlatl 33309
 Description: An atomic lattice with the covering property is an atomic lattice. (Contributed by NM, 5-Nov-2012.)
Assertion
Ref Expression
cvlatl

Proof of Theorem cvlatl
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2454 . . 3
2 eqid 2454 . . 3
3 eqid 2454 . . 3
4 eqid 2454 . . 3
51, 2, 3, 4iscvlat 33307 . 2
65simplbi 460 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 369   wcel 1758  wral 2799   class class class wbr 4401  cfv 5527  (class class class)co 6201  cbs 14293  cple 14365  cjn 15234  catm 33247  cal 33248  clc 33249 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-br 4402  df-iota 5490  df-fv 5535  df-ov 6204  df-cvlat 33306 This theorem is referenced by:  cvllat  33310  cvlexch3  33316  cvlexch4N  33317  cvlatexchb1  33318  cvlcvr1  33323  cvlcvrp  33324  cvlatcvr1  33325  cvlsupr2  33327  hlatl  33344
 Copyright terms: Public domain W3C validator