How do I write Ax ( P(x) and Q(x) ) in Coq?

I'm trying out Coq, but I'm not completely sure what I'm doing. Is:

Theorem new_theorem : forall x, P:Prop /\ Q:Prop

Equivalent to:

Ax ( P(x) and Q(x) )

(where A is supposed to be the universal quantifier).

Edit: I think they are.

From stackoverflow

• Are you having problems with the syntax?

  $ coqtop
  Welcome to Coq 8.1pl3 (Dec. 2007)
  
  Coq < Section Test.
  
  Coq < Variable X:Set.
  X is assumed
  
  Coq < Variables P Q:X -> Prop.
  P is assumed
  Q is assumed
  
  Coq < Theorem forall_test: forall x:X, P(x) /\ Q(x).
  1 subgoal
  
    X : Set
    P : X -> Prop
    Q : X -> Prop
    ============================
     forall x : X, P x /\ Q x
  
  forall_test <
  

• Well, to answer your question:

  Section test.
  
    Variable A : Type.           (* assume some universe A *)
    Variable P Q : A -> Prop.    (* and two predicates over A, P and Q *)
  
    Goal forall x, P x /\ Q x.   (* Ax, ( P(x) and Q(x) ) *)
  
  End test.