Theorem ml3le 1129

Description: Form of modular law that swaps two terms. (Contributed by NM, 1-Apr-2012.)

Assertion

Ref	Expression
ml3le	(a ∪ (b ∩ (c ∪ a))) ≤ (a ∪ (c ∩ (b ∪ a)))

Proof of Theorem ml3le

Step	Hyp	Ref	Expression
1		lear 161	. . . . 5 (b ∩ (c ∪ a)) ≤ (c ∪ a)
2	1	lelor 166	. . . 4 (a ∪ (b ∩ (c ∪ a))) ≤ (a ∪ (c ∪ a))
3		or12 80	. . . . 5 (a ∪ (c ∪ a)) = (c ∪ (a ∪ a))
4		oridm 110	. . . . . 6 (a ∪ a) = a
5	4	lor 70	. . . . 5 (c ∪ (a ∪ a)) = (c ∪ a)
6		orcom 73	. . . . 5 (c ∪ a) = (a ∪ c)
7	3, 5, 6	3tr 65	. . . 4 (a ∪ (c ∪ a)) = (a ∪ c)
8	2, 7	lbtr 139	. . 3 (a ∪ (b ∩ (c ∪ a))) ≤ (a ∪ c)
9		leor 159	. . . 4 a ≤ (b ∪ a)
10		leao1 162	. . . 4 (b ∩ (c ∪ a)) ≤ (b ∪ a)
11	9, 10	lel2or 170	. . 3 (a ∪ (b ∩ (c ∪ a))) ≤ (b ∪ a)
12	8, 11	ler2an 173	. 2 (a ∪ (b ∩ (c ∪ a))) ≤ ((a ∪ c) ∩ (b ∪ a))
13	9	mlduali 1128	. 2 ((a ∪ c) ∩ (b ∪ a)) = (a ∪ (c ∩ (b ∪ a)))
14	12, 13	lbtr 139	1 (a ∪ (b ∩ (c ∪ a))) ≤ (a ∪ (c ∩ (b ∪ a)))

This proof depends on syntax axioms:   ≤ wle 2   ∪ wo 6   ∩ wa 7

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-ml 1122

This proof depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is used by:  ml3  1130  dp15leme  1158  xdp15  1199  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208