Theorem ralimiaa 3101

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∀wral 3079

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

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

This theorem is referenced by:  ralrnmptw  7089  ralrnmpt  7091  tz7.48-2  8425  mptelixpg  8929  boxriin  8934  acnlem  10028  iundom2g  10519  konigthlem  10548  hashge2el2dif  14513  rlim2  15543  prdsbas3  17529  prdsdsval2  17532  ptbasfi  23738  ptunimpt  23752  voliun  25713  lgamgulmlem6  27198  riesz4i  32415  dmdbr6ati  32775  ctbssinf  38072