Theorem ralimia 3063

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)

Hypothesis

Ref	Expression
ralimia.1	⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))

Assertion

Ref	Expression
ralimia	⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralimia

Step	Hyp	Ref	Expression
1		ralimia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
2	1	a2i 14	. 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralimi2 3061	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

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

This theorem depends on definitions:  df-bi 207  df-ral 3045

This theorem is referenced by:  ralimiaa  3065  ralimi  3066  rr19.3v  3624  rr19.28v  3625  exfo  7043  ffvresb  7063  f1mpt  7202  weniso  7295  xpord2indlem  8087  ixpf  8854  ixpiunwdom  9501  tz9.12lem3  9704  dfac2a  10043  kmlem12  10075  axdc2lem  10361  ac6c4  10394  brdom6disj  10445  konigthlem  10481  arch  12399  cshw1  14746  serf0  15606  symgextfo  19319  baspartn  22857  ptcnplem  23524  spanuni  31506  lnopunilem1  31972  phpreu  37586  finixpnum  37587  poimirlem26  37628  indexa  37715  heiborlem5  37797  rngmgmbs4  37913  mzpincl  42710  dfac11  43038  mnurndlem1  44257  natlocalincr  46861  stgoldbwt  47764  2zrngnmlid2  48245