Translate the following inference to logic notation: For all x, if z drives a car, then z is poor. For all x, if z were poor, then z is driving a car. Thomas is not driving a car. Therefore Thomas is not poor.
forall x: P(x) -> Q(x). forall x: Q(x) -> P(x). ~P(a). Therefore ~Q(a).