Theorem ralimia 3073

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

Syntax hints:   → wi 4   ∈ wcel 2119  ∀wral 3053

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

This theorem depends on definitions:  df-bi 208  df-ral 3054

This theorem is referenced by:  ralimiaa  3075  ralimi  3076  rr19.3v  3605  rr19.28v  3606  exfo  7046  ffvresb  7067  f1mpt  7205  weniso  7298  xpord2indlem  8087  ixpf  8858  ixpiunwdom  9495  tz9.12lem3  9704  dfac2a  10043  kmlem12  10075  axdc2lem  10361  ac6c4  10394  brdom6disj  10445  konigthlem  10482  arch  12425  cshw1  14775  serf0  15634  symgextfo  19388  baspartn  22937  ptcnplem  23604  spanuni  31633  lnopunilem1  32099  phpreu  37971  finixpnum  37972  poimirlem26  38013  indexa  38100  heiborlem5  38182  rngmgmbs4  38298  mzpincl  43183  dfac11  43507  mnurndlem1  44725  natlocalincr  47321  stgoldbwt  48267  2zrngnmlid2  48748