let a, b, c, d be Integer; :: thesis: ( b divides a & d divides c implies b * d divides a * c )
assume that
A1: b divides a and
A2: d divides c ; :: thesis: b * d divides a * c
consider t being Integer such that
A3: b * t = a by A1;
consider z being Integer such that
A4: d * z = c by A2;
(b * d) * (t * z) = a * c by A3, A4;
hence b * d divides a * c ; :: thesis: verum