Theorem ralimia 3070

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∀wral 3051

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

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

This theorem is referenced by:  ralimiaa  3072  ralimi  3073  rr19.3v  3621  rr19.28v  3622  exfo  7050  ffvresb  7070  f1mpt  7207  weniso  7300  xpord2indlem  8089  ixpf  8858  ixpiunwdom  9495  tz9.12lem3  9701  dfac2a  10040  kmlem12  10072  axdc2lem  10358  ac6c4  10391  brdom6disj  10442  konigthlem  10479  arch  12398  cshw1  14745  serf0  15604  symgextfo  19351  baspartn  22898  ptcnplem  23565  spanuni  31619  lnopunilem1  32085  phpreu  37805  finixpnum  37806  poimirlem26  37847  indexa  37934  heiborlem5  38016  rngmgmbs4  38132  mzpincl  42976  dfac11  43304  mnurndlem1  44522  natlocalincr  47120  stgoldbwt  48022  2zrngnmlid2  48503