Theorem ralimiaa 3085

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 412	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	ralimia 3084	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3063

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3068

This theorem is referenced by:  ralrnmptw  6952  ralrnmpt  6954  tz7.48-2  8243  mptelixpg  8681  boxriin  8686  acnlem  9735  iundom2g  10227  konigthlem  10255  hashge2el2dif  14122  rlim2  15133  prdsbas3  17109  prdsdsval2  17112  ptbasfi  22640  ptunimpt  22654  voliun  24623  lgamgulmlem6  26088  riesz4i  30326  dmdbr6ati  30686  ctbssinf  35504