Theorem ralimiaa 3081

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 3079	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∀wral 3060

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

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

This theorem is referenced by:  ralrnmptw  7095  ralrnmpt  7097  tz7.48-2  8448  mptelixpg  8935  boxriin  8940  acnlem  10049  iundom2g  10541  konigthlem  10569  hashge2el2dif  14448  rlim2  15447  prdsbas3  17434  prdsdsval2  17437  ptbasfi  23404  ptunimpt  23418  voliun  25402  lgamgulmlem6  26878  riesz4i  31748  dmdbr6ati  32108  ctbssinf  36750