llnexchb2

Description: Line exchange property (compare cvlatexchb2 for atoms). (Contributed by NM, 17-Nov-2012)

	Ref	Expression
Hypotheses	llnexch.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	llnexch.j	$⊢ \underset{˙}{\lor} = join (K)$
	llnexch.m	$⊢ \underset{˙}{\land} = meet (K)$
	llnexch.a	$⊢ A = Atoms (K)$
	llnexch.n	$⊢ N = LLines (K)$
Assertion	llnexchb2	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} Z \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} Z)$

Proof

Step	Hyp	Ref	Expression
1		llnexch.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		llnexch.j	$⊢ \underset{˙}{\lor} = join (K)$
3		llnexch.m	$⊢ \underset{˙}{\land} = meet (K)$
4		llnexch.a	$⊢ A = Atoms (K)$
5		llnexch.n	$⊢ N = LLines (K)$
6		simp23	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to Z \in N$
7		simp1	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to K \in HL$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9	8 5	llnbase	$⊢ Z \in N \to Z \in {Base}_{K}$
10	6 9	syl	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to Z \in {Base}_{K}$
11	8 2 4 5	islln3	$⊢ (K \in HL \land Z \in {Base}_{K}) \to (Z \in N \leftrightarrow \exists p \in A \exists q \in A (p \neq q \land Z = p \underset{˙}{\lor} q))$
12	7 10 11	syl2anc	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to (Z \in N \leftrightarrow \exists p \in A \exists q \in A (p \neq q \land Z = p \underset{˙}{\lor} q))$
13	6 12	mpbid	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to \exists p \in A \exists q \in A (p \neq q \land Z = p \underset{˙}{\lor} q)$
14		simp3r	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to X \neq Z$
15	14	necomd	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to Z \neq X$
16		simp11	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to K \in HL$
17	16	hllatd	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to K \in Lat$
18		simp2l	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to p \in A$
19	8 4	atbase	$⊢ p \in A \to p \in {Base}_{K}$
20	18 19	syl	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to p \in {Base}_{K}$
21		simp2r	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to q \in A$
22	8 4	atbase	$⊢ q \in A \to q \in {Base}_{K}$
23	21 22	syl	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to q \in {Base}_{K}$
24		simp121	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to X \in N$
25	8 5	llnbase	$⊢ X \in N \to X \in {Base}_{K}$
26	24 25	syl	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to X \in {Base}_{K}$
27	8 1 2	latjle12	$⊢ (K \in Lat \land (p \in {Base}_{K} \land q \in {Base}_{K} \land X \in {Base}_{K})) \to ((p \underset{˙}{\leq} X \land q \underset{˙}{\leq} X) \leftrightarrow (p \underset{˙}{\lor} q) \underset{˙}{\leq} X)$
28	17 20 23 26 27	syl13anc	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to ((p \underset{˙}{\leq} X \land q \underset{˙}{\leq} X) \leftrightarrow (p \underset{˙}{\lor} q) \underset{˙}{\leq} X)$
29		simp3	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to p \neq q$
30	2 4 5	llni2	$⊢ ((K \in HL \land p \in A \land q \in A) \land p \neq q) \to p \underset{˙}{\lor} q \in N$
31	16 18 21 29 30	syl31anc	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to p \underset{˙}{\lor} q \in N$
32	1 5	llncmp	$⊢ (K \in HL \land p \underset{˙}{\lor} q \in N \land X \in N) \to ((p \underset{˙}{\lor} q) \underset{˙}{\leq} X \leftrightarrow p \underset{˙}{\lor} q = X)$
33	16 31 24 32	syl3anc	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to ((p \underset{˙}{\lor} q) \underset{˙}{\leq} X \leftrightarrow p \underset{˙}{\lor} q = X)$
34	28 33	bitr2d	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to (p \underset{˙}{\lor} q = X \leftrightarrow (p \underset{˙}{\leq} X \land q \underset{˙}{\leq} X))$
35	34	necon3abid	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to (p \underset{˙}{\lor} q \neq X \leftrightarrow \neg (p \underset{˙}{\leq} X \land q \underset{˙}{\leq} X))$
36		ianor	$⊢ \neg (p \underset{˙}{\leq} X \land q \underset{˙}{\leq} X) \leftrightarrow (\neg p \underset{˙}{\leq} X \lor \neg q \underset{˙}{\leq} X)$
37	35 36	bitrdi	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to (p \underset{˙}{\lor} q \neq X \leftrightarrow (\neg p \underset{˙}{\leq} X \lor \neg q \underset{˙}{\leq} X))$
38		simpl11	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg p \underset{˙}{\leq} X) \to K \in HL$
39	24	adantr	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg p \underset{˙}{\leq} X) \to X \in N$
40		simp122	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to Y \in N$
41	40	adantr	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg p \underset{˙}{\leq} X) \to Y \in N$
42		simpl2l	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg p \underset{˙}{\leq} X) \to p \in A$
43		simpl2r	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg p \underset{˙}{\leq} X) \to q \in A$
44		simpr	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg p \underset{˙}{\leq} X) \to \neg p \underset{˙}{\leq} X$
45		simp13l	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to X \underset{˙}{\land} Y \in A$
46	45	adantr	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg p \underset{˙}{\leq} X) \to X \underset{˙}{\land} Y \in A$
47	1 2 3 4 5	llnexchb2lem	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in A \land q \in A \land \neg p \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (p \underset{˙}{\lor} q) \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (p \underset{˙}{\lor} q))$
48	38 39 41 42 43 44 46 47	syl331anc	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg p \underset{˙}{\leq} X) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (p \underset{˙}{\lor} q) \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (p \underset{˙}{\lor} q))$
49	48	ex	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to (\neg p \underset{˙}{\leq} X \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (p \underset{˙}{\lor} q) \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (p \underset{˙}{\lor} q)))$
50		simpl11	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg q \underset{˙}{\leq} X) \to K \in HL$
51	24	adantr	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg q \underset{˙}{\leq} X) \to X \in N$
52	40	adantr	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg q \underset{˙}{\leq} X) \to Y \in N$
53		simpl2r	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg q \underset{˙}{\leq} X) \to q \in A$
54		simpl2l	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg q \underset{˙}{\leq} X) \to p \in A$
55		simpr	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg q \underset{˙}{\leq} X) \to \neg q \underset{˙}{\leq} X$
56	45	adantr	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg q \underset{˙}{\leq} X) \to X \underset{˙}{\land} Y \in A$
57	1 2 3 4 5	llnexchb2lem	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (q \in A \land p \in A \land \neg q \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (q \underset{˙}{\lor} p) \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (q \underset{˙}{\lor} p))$
58	50 51 52 53 54 55 56 57	syl331anc	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg q \underset{˙}{\leq} X) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (q \underset{˙}{\lor} p) \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (q \underset{˙}{\lor} p))$
59	2 4	hlatjcom	$⊢ (K \in HL \land p \in A \land q \in A) \to p \underset{˙}{\lor} q = q \underset{˙}{\lor} p$
60	50 54 53 59	syl3anc	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg q \underset{˙}{\leq} X) \to p \underset{˙}{\lor} q = q \underset{˙}{\lor} p$
61	60	breq2d	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg q \underset{˙}{\leq} X) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (p \underset{˙}{\lor} q) \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{\leq} (q \underset{˙}{\lor} p))$
62	60	oveq2d	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg q \underset{˙}{\leq} X) \to X \underset{˙}{\land} (p \underset{˙}{\lor} q) = X \underset{˙}{\land} (q \underset{˙}{\lor} p)$
63	62	eqeq2d	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg q \underset{˙}{\leq} X) \to (X \underset{˙}{\land} Y = X \underset{˙}{\land} (p \underset{˙}{\lor} q) \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (q \underset{˙}{\lor} p))$
64	58 61 63	3bitr4d	$⊢ (((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \land \neg q \underset{˙}{\leq} X) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (p \underset{˙}{\lor} q) \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (p \underset{˙}{\lor} q))$
65	64	ex	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to (\neg q \underset{˙}{\leq} X \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (p \underset{˙}{\lor} q) \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (p \underset{˙}{\lor} q)))$
66	49 65	jaod	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to ((\neg p \underset{˙}{\leq} X \lor \neg q \underset{˙}{\leq} X) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (p \underset{˙}{\lor} q) \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (p \underset{˙}{\lor} q)))$
67	37 66	sylbid	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to (p \underset{˙}{\lor} q \neq X \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (p \underset{˙}{\lor} q) \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (p \underset{˙}{\lor} q)))$
68		neeq1	$⊢ Z = p \underset{˙}{\lor} q \to (Z \neq X \leftrightarrow p \underset{˙}{\lor} q \neq X)$
69		breq2	$⊢ Z = p \underset{˙}{\lor} q \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} Z \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{\leq} (p \underset{˙}{\lor} q))$
70		oveq2	$⊢ Z = p \underset{˙}{\lor} q \to X \underset{˙}{\land} Z = X \underset{˙}{\land} (p \underset{˙}{\lor} q)$
71	70	eqeq2d	$⊢ Z = p \underset{˙}{\lor} q \to (X \underset{˙}{\land} Y = X \underset{˙}{\land} Z \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (p \underset{˙}{\lor} q))$
72	69 71	bibi12d	$⊢ Z = p \underset{˙}{\lor} q \to (((X \underset{˙}{\land} Y) \underset{˙}{\leq} Z \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} Z) \leftrightarrow ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (p \underset{˙}{\lor} q) \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (p \underset{˙}{\lor} q)))$
73	68 72	imbi12d	$⊢ Z = p \underset{˙}{\lor} q \to ((Z \neq X \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} Z \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} Z)) \leftrightarrow (p \underset{˙}{\lor} q \neq X \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (p \underset{˙}{\lor} q) \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (p \underset{˙}{\lor} q))))$
74	67 73	syl5ibrcom	$⊢ ((K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \land (p \in A \land q \in A) \land p \neq q) \to (Z = p \underset{˙}{\lor} q \to (Z \neq X \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} Z \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} Z)))$
75	74	3exp	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to ((p \in A \land q \in A) \to (p \neq q \to (Z = p \underset{˙}{\lor} q \to (Z \neq X \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} Z \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} Z)))))$
76	75	imp4a	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to ((p \in A \land q \in A) \to ((p \neq q \land Z = p \underset{˙}{\lor} q) \to (Z \neq X \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} Z \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} Z))))$
77	76	rexlimdvv	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to (\exists p \in A \exists q \in A (p \neq q \land Z = p \underset{˙}{\lor} q) \to (Z \neq X \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} Z \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} Z)))$
78	13 15 77	mp2d	$⊢ (K \in HL \land (X \in N \land Y \in N \land Z \in N) \land (X \underset{˙}{\land} Y \in A \land X \neq Z)) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} Z \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} Z)$

Metamath Proof Explorer

Theorem llnexchb2

Proof