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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3060

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

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

This theorem is referenced by:  ralrnmptw  7049  ralrnmpt  7051  tz7.48-2  8393  mptelixpg  8880  boxriin  8885  acnlem  9993  iundom2g  10485  konigthlem  10513  hashge2el2dif  14391  rlim2  15390  prdsbas3  17377  prdsdsval2  17380  ptbasfi  22969  ptunimpt  22983  voliun  24955  lgamgulmlem6  26420  riesz4i  31068  dmdbr6ati  31428  ctbssinf  35950