Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  omlmod1i2N Structured version   Unicode version

Theorem omlmod1i2N 29985
 Description: Analog of modular law atmod1i2 30583 that holds in any OML. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
omlmod.b
omlmod.l
omlmod.j
omlmod.m
omlmod.c
Assertion
Ref Expression
omlmod1i2N

Proof of Theorem omlmod1i2N
StepHypRef Expression
1 simp1 957 . . 3
2 simp23 992 . . 3
3 simp21 990 . . 3
4 simp22 991 . . 3
5 simp3l 985 . . . . 5
6 omlmod.b . . . . . . 7
7 omlmod.l . . . . . . 7
8 omlmod.c . . . . . . 7
96, 7, 8lecmtN 29981 . . . . . 6
101, 3, 2, 9syl3anc 1184 . . . . 5
115, 10mpd 15 . . . 4
126, 8cmtcomN 29974 . . . . 5
131, 3, 2, 12syl3anc 1184 . . . 4
1411, 13mpbid 202 . . 3
15 simp3r 986 . . . 4
166, 8cmtcomN 29974 . . . . 5
171, 4, 2, 16syl3anc 1184 . . . 4
1815, 17mpbid 202 . . 3
19 omlmod.j . . . 4
20 omlmod.m . . . 4
216, 19, 20, 8omlfh1N 29983 . . 3
221, 2, 3, 4, 14, 18, 21syl132anc 1202 . 2
23 omllat 29967 . . . 4