Theorem mlduali 1128

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

Hypothesis

Ref	Expression
mlduali.1	a ≤ c

Assertion

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

Proof of Theorem mlduali

Step	Hyp	Ref	Expression
1		ax-a2 31	. . . 4 (a ∪ b) = (b ∪ a)
2	1	ran 78	. . 3 ((a ∪ b) ∩ c) = ((b ∪ a) ∩ c)
3		ancom 74	. . 3 ((b ∪ a) ∩ c) = (c ∩ (b ∪ a))
4		mlduali.1	. . . 4 a ≤ c
5	4	mldual2i 1127	. . 3 (c ∩ (b ∪ a)) = ((c ∩ b) ∪ a)
6	2, 3, 5	3tr 65	. 2 ((a ∪ b) ∩ c) = ((c ∩ b) ∪ a)
7		ancom 74	. . 3 (c ∩ b) = (b ∩ c)
8	7	ror 71	. 2 ((c ∩ b) ∪ a) = ((b ∩ c) ∪ a)
9		orcom 73	. 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:  ml3le  1129  modexp  1152  dp15lema  1154  dp35leme  1173  xdp15  1199  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod2  1215  testmod2expanded  1216