Theorem ralimiaa 3127

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∀wral 3106

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 210  df-an 400  df-ral 3111

This theorem is referenced by:  ralrnmptw  6837  ralrnmpt  6839  tz7.48-2  8061  mptelixpg  8482  boxriin  8487  acnlem  9459  iundom2g  9951  konigthlem  9979  hashge2el2dif  13834  rlim2  14845  prdsbas3  16746  prdsdsval2  16749  ptbasfi  22186  ptunimpt  22200  voliun  24158  lgamgulmlem6  25619  riesz4i  29846  dmdbr6ati  30206  ctbssinf  34823