Theorem ralimia 3080

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3061

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 3062

This theorem is referenced by:  ralimiaa  3082  ralimi  3083  rr19.3v  3667  rr19.28v  3668  exfo  7125  ffvresb  7145  f1mpt  7281  weniso  7374  xpord2indlem  8172  ixpf  8960  ixpiunwdom  9630  tz9.12lem3  9829  dfac2a  10170  kmlem12  10202  axdc2lem  10488  ac6c4  10521  brdom6disj  10572  konigthlem  10608  arch  12523  cshw1  14860  serf0  15717  symgextfo  19440  baspartn  22961  ptcnplem  23629  spanuni  31563  lnopunilem1  32029  phpreu  37611  finixpnum  37612  poimirlem26  37653  indexa  37740  heiborlem5  37822  rngmgmbs4  37938  mzpincl  42745  dfac11  43074  mnurndlem1  44300  natlocalincr  46891  stgoldbwt  47763  2zrngnmlid2  48173