How to prove (forall x, P x /\ Q x) -> (forall x, P x) [In Coq]

How does one prove (forall x, P x /\ Q x) -> (forall x, P x) in Coq? Been trying for hours and can't figure out how to break down the antecedent to something that Coq can digest. (I'm a newb, obviously :)

From stackoverflow

• Try

  elim (H x).
  

• Actually, I figured this one out when I found this:

  Mathematics for Computer Scientists 2

  In lesson 5 he solves the exact same problem and uses "cut (P x /\ Q x)" which re-writes the goal from "P x" to "P x /\ Q x -> P x". From there you can do some manipulations and when the goal is just "P x /\ Q x" you can apply "forall x : P x /\ Q x" and the rest is straightforward.

• You can do it more quickly by just applying H, but this script should be more clear.

  Lemma foo : forall (A:Type) (P Q: A-> Prop), (forall x, P x /\ Q x) -> (forall x, P x).
  intros.
  destruct (H x). 
  exact H0.
  Qed.
  

• Assume ForAll x: P(x) /\ Q(x)
     var x; 
        P(x) //because you assumed it earlier
     ForAll x: P(x)
  (ForAll x: P(x) /\ Q(x)) => (ForAll x: P(x))
  

  Intuitivly, if for all x, P(x) AND Q(x) hold, then for all x, P(x) holds.