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

 Description: Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.)
Assertion
Ref Expression

Dummy variable is distinct from all other variables.
StepHypRef Expression
2 ax-rnegex 7147 . . . 4
4 simpl3 944 . . . . . . 7
5 simpl1 942 . . . . . . 7
64, 5readdcld 7210 . . . . . 6
7 simpl2 943 . . . . . . 7
84, 7readdcld 7210 . . . . . 6
9 simprl 498 . . . . . 6
10 axltadd 7249 . . . . . 6
116, 8, 9, 10syl3anc 1170 . . . . 5
129recnd 7209 . . . . . . 7
134recnd 7209 . . . . . . 7
145recnd 7209 . . . . . . 7
1512, 13, 14addassd 7203 . . . . . 6
167recnd 7209 . . . . . . 7
1712, 13, 16addassd 7203 . . . . . 6
1815, 17breq12d 3806 . . . . 5
1911, 18sylibrd 167 . . . 4
20 simprr 499 . . . . . . . 8
21 addcom 7312 . . . . . . . . . 10
2221eqeq1d 2090 . . . . . . . . 9
2313, 12, 22syl2anc 403 . . . . . . . 8
2420, 23mpbid 145 . . . . . . 7
2524oveq1d 5558 . . . . . 6
2614addid2d 7325 . . . . . 6
2725, 26eqtrd 2114 . . . . 5
2824oveq1d 5558 . . . . . 6
2916addid2d 7325 . . . . . 6
3028, 29eqtrd 2114 . . . . 5
3127, 30breq12d 3806 . . . 4
3219, 31sylibd 147 . . 3
333, 32rexlimddv 2482 . 2
341, 33impbid 127 1