Theorem ralimiaa 3098

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142  ∀wral 3076

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3077

This theorem is referenced by:  ralrnmptw  7075  ralrnmpt  7077  tz7.48-2  8413  mptelixpg  8917  boxriin  8922  acnlem  10004  iundom2g  10497  konigthlem  10526  hashge2el2dif  14493  rlim2  15523  prdsbas3  17510  prdsdsval2  17513  ptbasfi  23641  ptunimpt  23655  voliun  25616  lgamgulmlem6  27098  riesz4i  32266  dmdbr6ati  32626  ctbssinf  37900