Theorem mldual2i 1127

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

Hypothesis

Ref	Expression
mlduali.1	a ≤ c

Assertion

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

Proof of Theorem mldual2i

Step	Hyp	Ref	Expression
1		mldual 1124	. 2 (c ∩ (b ∪ (c ∩ a))) = ((c ∩ b) ∪ (c ∩ a))
2		lear 161	. . . . 5 (c ∩ a) ≤ a
3		mlduali.1	. . . . . 6 a ≤ c
4		leid 148	. . . . . 6 a ≤ a
5	3, 4	ler2an 173	. . . . 5 a ≤ (c ∩ a)
6	2, 5	lebi 145	. . . 4 (c ∩ a) = a
7	6	lor 70	. . 3 (b ∪ (c ∩ a)) = (b ∪ a)
8	7	lan 77	. 2 (c ∩ (b ∪ (c ∩ a))) = (c ∩ (b ∪ a))
9	6	lor 70	. 2 ((c ∩ b) ∪ (c ∩ a)) = ((c ∩ b) ∪ a)
10	1, 8, 9	3tr2 64	1 (c ∩ (b ∪ a)) = ((c ∩ b) ∪ a)

Syntax hints:   = wb 1   ≤ wle 2   ∪ wo 6   ∩ wa 7

This theorem was proved from 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 theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is referenced by:  mlduali  1128  dp15lemf  1159  dp53lema  1163  dp53leme  1167  dp53lemf  1168  dp35lemd  1174  dp35lem0  1179  dp41lemc0  1184  dp41leme  1187  dp41lemk  1192  dp32  1196  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod2  1215  testmod2expanded  1216