dlatmjdi - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dlatmjdi		Structured version Visualization version Unicode version

Theorem dlatmjdi 17194

Description: In a distributive lattice, meets distribute over joins. (Contributed by Stefan O'Rear, 30-Jan-2015.)

**Assertion**
Ref	Expression
dlatmjdi	DLat $/\$ $/\$ $/\$ $./\$ $.\/$ $./\$ $.\/$ $./\$

Proof of Theorem dlatmjdi Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isdlat.b	. . . 4
2		isdlat.j	. . . 4 $.\/$
3		isdlat.m	. . . 4 $./\$
4	1, 2, 3	isdlat 17193	. . 3 DLat $/\$ $./\$ $.\/$ $./\$ $.\/$ $./\$
5	4	simprbi 480	. 2 DLat $./\$ $.\/$ $./\$ $.\/$ $./\$
6		oveq1 6657	. . . 4 $./\$ $.\/$ $./\$ $.\/$
7		oveq1 6657	. . . . 5 $./\$ $./\$
8		oveq1 6657	. . . . 5 $./\$ $./\$
9	7, 8	oveq12d 6668	. . . 4 $./\$ $.\/$ $./\$ $./\$ $.\/$ $./\$
10	6, 9	eqeq12d 2637	. . 3 $./\$ $.\/$ $./\$ $.\/$ $./\$ $./\$ $.\/$ $./\$ $.\/$ $./\$
11		oveq1 6657	. . . . 5 $.\/$ $.\/$
12	11	oveq2d 6666	. . . 4 $./\$ $.\/$ $./\$ $.\/$
13		oveq2 6658	. . . . 5 $./\$ $./\$
14	13	oveq1d 6665	. . . 4 $./\$ $.\/$ $./\$ $./\$ $.\/$ $./\$
15	12, 14	eqeq12d 2637	. . 3 $./\$ $.\/$ $./\$ $.\/$ $./\$ $./\$ $.\/$ $./\$ $.\/$ $./\$
16		oveq2 6658	. . . . 5 $.\/$ $.\/$
17	16	oveq2d 6666	. . . 4 $./\$ $.\/$ $./\$ $.\/$
18		oveq2 6658	. . . . 5 $./\$ $./\$
19	18	oveq2d 6666	. . . 4 $./\$ $.\/$ $./\$ $./\$ $.\/$ $./\$
20	17, 19	eqeq12d 2637	. . 3 $./\$ $.\/$ $./\$ $.\/$ $./\$ $./\$ $.\/$ $./\$ $.\/$ $./\$
21	10, 15, 20	rspc3v 3325	. 2 $/\$ $/\$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $./\$ $.\/$ $./\$ $.\/$ $./\$
22	5, 21	mpan9 486	1 DLat $/\$ $/\$ $/\$ $./\$ $.\/$ $./\$ $.\/$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wral 2912

cfv 5888 (class class class)co 6650

cbs 15857

cjn 16944

cmee 16945

clat 17045 DLatcdlat 17191

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-nul 4789

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 df-dlat 17192

This theorem is referenced by: dlatjmdi 17197