Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltsopi Unicode version

Theorem ltsopi 6572
 Description: Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.)
Assertion
Ref Expression
ltsopi

Proof of Theorem ltsopi
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elirrv 4299 . . . . . 6
2 ltpiord 6571 . . . . . . 7
32anidms 389 . . . . . 6
41, 3mtbiri 633 . . . . 5
54adantl 271 . . . 4
6 pion 6562 . . . . . . . 8
7 ontr1 4152 . . . . . . . 8
86, 7syl 14 . . . . . . 7
983ad2ant3 962 . . . . . 6
10 ltpiord 6571 . . . . . . . 8
11103adant3 959 . . . . . . 7
12 ltpiord 6571 . . . . . . . 8
13123adant1 957 . . . . . . 7
1411, 13anbi12d 457 . . . . . 6
15 ltpiord 6571 . . . . . . 7
16153adant2 958 . . . . . 6
179, 14, 163imtr4d 201 . . . . 5
1817adantl 271 . . . 4
195, 18ispod 4067 . . 3
20 pinn 6561 . . . . . 6
21 pinn 6561 . . . . . 6
22 nntri3or 6137 . . . . . 6
2320, 21, 22syl2an 283 . . . . 5
24 biidd 170 . . . . . 6
25 ltpiord 6571 . . . . . . 7
2625ancoms 264 . . . . . 6
2710, 24, 263orbi123d 1243 . . . . 5
2823, 27mpbird 165 . . . 4