theorem :: INT_4:45

for m1, m2, m3, a, b, c being Integer st m1 <> 0 & m2 <> 0 & m3 <> 0 & ( not m1 gcd m2 divides a - b or not m1 gcd m3 divides a - c or not m2 gcd m3 divides b - c ) holds
for x being Integer holds
( not (x - a) mod m1 = 0 or not (x - b) mod m2 = 0 or not (x - c) mod m3 = 0 ) by Th41;