Theorem mldual2i 1125

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 1122	. 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 1120

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  1126  dp15lemf  1157  dp53lema  1161  dp53leme  1165  dp53lemf  1166  dp35lemd  1172  dp35lem0  1177  dp41lemc0  1182  dp41leme  1185  dp41lemk  1190  dp32  1194  xdp41  1196  xdp15  1197  xdp53  1198  xxdp41  1199  xxdp15  1200  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  testmod2  1213  testmod2expanded  1214