Theorem ralimiaa 3132

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)

Hypothesis

Ref	Expression
ralimiaa.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)

Assertion

Ref	Expression
ralimiaa	⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralimiaa

Step	Hyp	Ref	Expression
1		ralimiaa.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
2	1	ex 403	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	ralimia 3131	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2106  ∀wral 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853

This theorem depends on definitions:  df-bi 199  df-an 387  df-ral 3094

This theorem is referenced by:  ralrnmpt  6632  tz7.48-2  7820  mptelixpg  8231  boxriin  8236  acnlem  9204  iundom2g  9697  konigthlem  9725  hashge2el2dif  13576  rlim2  14635  prdsbas3  16527  prdsdsval2  16530  ptbasfi  21793  ptunimpt  21807  voliun  23758  lgamgulmlem6  25212  riesz4i  29494  dmdbr6ati  29854