2llnjaN

Description: The join of two different lattice lines in a lattice plane equals the plane (version of 2llnjN in terms of atoms). (Contributed by NM, 5-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2llnja.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	2llnja.j	$⊢ \underset{˙}{\lor} = join (K)$
	2llnja.a	$⊢ A = Atoms (K)$
	2llnja.n	$⊢ N = LLines (K)$
	2llnja.p	$⊢ P = LPlanes (K)$
Assertion	2llnjaN	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T) = W$

Proof

Step	Hyp	Ref	Expression
1		2llnja.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		2llnja.j	$⊢ \underset{˙}{\lor} = join (K)$
3		2llnja.a	$⊢ A = Atoms (K)$
4		2llnja.n	$⊢ N = LLines (K)$
5		2llnja.p	$⊢ P = LPlanes (K)$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7		simpl1l	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to K \in HL$
8	7	hllatd	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to K \in Lat$
9		simpl21	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to Q \in A$
10		simpl22	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to R \in A$
11	6 2 3	hlatjcl	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
12	7 9 10 11	syl3anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
13		simpl31	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to S \in A$
14		simpl32	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to T \in A$
15	6 2 3	hlatjcl	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T \in {Base}_{K}$
16	7 13 14 15	syl3anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to S \underset{˙}{\lor} T \in {Base}_{K}$
17	6 2	latjcl	$⊢ (K \in Lat \land Q \underset{˙}{\lor} R \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K}) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T) \in {Base}_{K}$
18	8 12 16 17	syl3anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T) \in {Base}_{K}$
19		simpl1r	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to W \in P$
20	6 5	lplnbase	$⊢ W \in P \to W \in {Base}_{K}$
21	19 20	syl	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to W \in {Base}_{K}$
22		simpr1	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\leq} W$
23		simpr2	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to (S \underset{˙}{\lor} T) \underset{˙}{\leq} W$
24	6 1 2	latjle12	$⊢ (K \in Lat \land (Q \underset{˙}{\lor} R \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K} \land W \in {Base}_{K})) \to (((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W) \leftrightarrow ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} W)$
25	8 12 16 21 24	syl13anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to (((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W) \leftrightarrow ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} W)$
26	22 23 25	mpbi2and	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} W$
27	6 3	atbase	$⊢ T \in A \to T \in {Base}_{K}$
28	14 27	syl	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to T \in {Base}_{K}$
29	6 2	latjcl	$⊢ (K \in Lat \land Q \underset{˙}{\lor} R \in {Base}_{K} \land T \in {Base}_{K}) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} T \in {Base}_{K}$
30	8 12 28 29	syl3anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} T \in {Base}_{K}$
31	6 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
32	13 31	syl	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to S \in {Base}_{K}$
33	6 1 2	latlej2	$⊢ (K \in Lat \land S \in {Base}_{K} \land T \in {Base}_{K}) \to T \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
34	8 32 28 33	syl3anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to T \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
35	6 1 2	latjlej2	$⊢ (K \in Lat \land (T \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K})) \to (T \underset{˙}{\leq} (S \underset{˙}{\lor} T) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} T) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T)))$
36	8 28 16 12 35	syl13anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to (T \underset{˙}{\leq} (S \underset{˙}{\lor} T) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} T) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T)))$
37	34 36	mpd	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} T) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T))$
38	6 1 8 30 18 21 37 26	lattrd	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} T) \underset{˙}{\leq} W$
39	38	3adant3	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} T) \underset{˙}{\leq} W$
40		simp11l	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to K \in HL$
41		simp121	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to Q \in A$
42		simp122	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to R \in A$
43		simp132	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to T \in A$
44		simp123	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to Q \neq R$
45		simp23	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T$
46		simpl3	$⊢ ((((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
47		simpr	$⊢ ((((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
48	6 1 2	latjle12	$⊢ (K \in Lat \land (S \in {Base}_{K} \land T \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K})) \to ((S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
49	8 32 28 12 48	syl13anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to ((S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
50	49	3adant3	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to ((S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
51	50	adantr	$⊢ ((((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to ((S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
52	46 47 51	mpbi2and	$⊢ ((((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to (S \underset{˙}{\lor} T) \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
53		simpl3	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to (S \in A \land T \in A \land S \neq T)$
54	1 2 3	ps-1	$⊢ (K \in HL \land (S \in A \land T \in A \land S \neq T) \land (Q \in A \land R \in A)) \to ((S \underset{˙}{\lor} T) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow S \underset{˙}{\lor} T = Q \underset{˙}{\lor} R)$
55	7 53 9 10 54	syl112anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to ((S \underset{˙}{\lor} T) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow S \underset{˙}{\lor} T = Q \underset{˙}{\lor} R)$
56	55	3adant3	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to ((S \underset{˙}{\lor} T) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow S \underset{˙}{\lor} T = Q \underset{˙}{\lor} R)$
57	56	adantr	$⊢ ((((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to ((S \underset{˙}{\lor} T) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow S \underset{˙}{\lor} T = Q \underset{˙}{\lor} R)$
58	52 57	mpbid	$⊢ ((((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to S \underset{˙}{\lor} T = Q \underset{˙}{\lor} R$
59	58	eqcomd	$⊢ ((((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to Q \underset{˙}{\lor} R = S \underset{˙}{\lor} T$
60	59	ex	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to (T \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \to Q \underset{˙}{\lor} R = S \underset{˙}{\lor} T)$
61	60	necon3ad	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to (Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T \to \neg T \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
62	45 61	mpd	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to \neg T \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
63	1 2 3 5	lplni2	$⊢ (K \in HL \land (Q \in A \land R \in A \land T \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} T \in P$
64	40 41 42 43 44 62 63	syl132anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} T \in P$
65		simp11r	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to W \in P$
66	1 5	lplncmp	$⊢ (K \in HL \land (Q \underset{˙}{\lor} R) \underset{˙}{\lor} T \in P \land W \in P) \to (((Q \underset{˙}{\lor} R) \underset{˙}{\lor} T) \underset{˙}{\leq} W \leftrightarrow (Q \underset{˙}{\lor} R) \underset{˙}{\lor} T = W)$
67	40 64 65 66	syl3anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to (((Q \underset{˙}{\lor} R) \underset{˙}{\lor} T) \underset{˙}{\leq} W \leftrightarrow (Q \underset{˙}{\lor} R) \underset{˙}{\lor} T = W)$
68	39 67	mpbid	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} T = W$
69	37	3adant3	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} T) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T))$
70	68 69	eqbrtrrd	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to W \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T))$
71	70	3expia	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to (S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \to W \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T)))$
72	6 2	latjcl	$⊢ (K \in Lat \land Q \underset{˙}{\lor} R \in {Base}_{K} \land S \in {Base}_{K}) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in {Base}_{K}$
73	8 12 32 72	syl3anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in {Base}_{K}$
74	6 1 2	latlej1	$⊢ (K \in Lat \land S \in {Base}_{K} \land T \in {Base}_{K}) \to S \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
75	8 32 28 74	syl3anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to S \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
76	6 1 2	latjlej2	$⊢ (K \in Lat \land (S \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K})) \to (S \underset{˙}{\leq} (S \underset{˙}{\lor} T) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T)))$
77	8 32 16 12 76	syl13anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to (S \underset{˙}{\leq} (S \underset{˙}{\lor} T) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T)))$
78	75 77	mpd	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T))$
79	6 1 8 73 18 21 78 26	lattrd	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S) \underset{˙}{\leq} W$
80	79	3adant3	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S) \underset{˙}{\leq} W$
81		simp11l	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to K \in HL$
82		simp121	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to Q \in A$
83		simp122	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to R \in A$
84		simp131	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to S \in A$
85		simp123	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to Q \neq R$
86		simp3	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
87	1 2 3 5	lplni2	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A) \land (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P$
88	81 82 83 84 85 86 87	syl132anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P$
89		simp11r	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to W \in P$
90	1 5	lplncmp	$⊢ (K \in HL \land (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S \in P \land W \in P) \to (((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S) \underset{˙}{\leq} W \leftrightarrow (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S = W)$
91	81 88 89 90	syl3anc	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to (((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S) \underset{˙}{\leq} W \leftrightarrow (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S = W)$
92	80 91	mpbid	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S = W$
93	78	3adant3	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T))$
94	92 93	eqbrtrrd	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to W \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T))$
95	94	3expia	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to (\neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \to W \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T)))$
96	71 95	pm2.61d	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to W \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T))$
97	6 1 8 18 21 26 96	latasymd	$⊢ (((K \in HL \land W \in P) \land (Q \in A \land R \in A \land Q \neq R) \land (S \in A \land T \in A \land S \neq T)) \land ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} W \land (S \underset{˙}{\lor} T) \underset{˙}{\leq} W \land Q \underset{˙}{\lor} R \neq S \underset{˙}{\lor} T)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} T) = W$

Metamath Proof Explorer

Theorem 2llnjaN

Proof