Theorem ralimia 3064

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

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

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 3046

This theorem is referenced by:  ralimiaa  3066  ralimi  3067  rr19.3v  3636  rr19.28v  3637  exfo  7080  ffvresb  7100  f1mpt  7239  weniso  7332  xpord2indlem  8129  ixpf  8896  ixpiunwdom  9550  tz9.12lem3  9749  dfac2a  10090  kmlem12  10122  axdc2lem  10408  ac6c4  10441  brdom6disj  10492  konigthlem  10528  arch  12446  cshw1  14794  serf0  15654  symgextfo  19359  baspartn  22848  ptcnplem  23515  spanuni  31480  lnopunilem1  31946  phpreu  37605  finixpnum  37606  poimirlem26  37647  indexa  37734  heiborlem5  37816  rngmgmbs4  37932  mzpincl  42729  dfac11  43058  mnurndlem1  44277  natlocalincr  46881  stgoldbwt  47781  2zrngnmlid2  48249