Theorem ralimiaa 3107

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∀wral 3085

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3086

This theorem is referenced by:  ralrnmptw  7090  ralrnmpt  7092  tz7.48-2  8429  mptelixpg  8933  boxriin  8938  acnlem  10032  iundom2g  10524  konigthlem  10553  hashge2el2dif  14517  rlim2  15547  prdsbas3  17534  prdsdsval2  17537  ptbasfi  23707  ptunimpt  23721  voliun  25682  lgamgulmlem6  27164  riesz4i  32356  dmdbr6ati  32716  ctbssinf  37940