Theorem mli 1126

Description: Inference version of modular law. (Contributed by NM, 1-Apr-2012.)

Hypothesis

Ref	Expression
mli.1	c ≤ a

Assertion

Ref	Expression
mli	((a ∩ b) ∪ c) = (a ∩ (b ∪ c))

Proof of Theorem mli

Step	Hyp	Ref	Expression
1		ancom 74	. . . 4 (a ∩ b) = (b ∩ a)
2	1	ror 71	. . 3 ((a ∩ b) ∪ c) = ((b ∩ a) ∪ c)
3		orcom 73	. . 3 ((b ∩ a) ∪ c) = (c ∪ (b ∩ a))
4		mli.1	. . . 4 c ≤ a
5	4	ml2i 1125	. . 3 (c ∪ (b ∩ a)) = ((c ∪ b) ∩ a)
6	2, 3, 5	3tr 65	. 2 ((a ∩ b) ∪ c) = ((c ∪ b) ∩ a)
7		orcom 73	. . 3 (c ∪ b) = (b ∪ c)
8	7	ran 78	. 2 ((c ∪ b) ∩ a) = ((b ∪ c) ∩ a)
9		ancom 74	. 2 ((b ∪ c) ∩ a) = (a ∩ (b ∪ c))
10	6, 8, 9	3tr 65	1 ((a ∩ b) ∪ c) = (a ∩ (b ∪ c))

This proof depends on syntax axioms:   = wb 1   ≤ 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:  dp41lemf  1188  xdp41  1198  xxdp41  1201  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod  1213  testmod3  1217