Theorem ralimia 3101

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 15	. 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralimi2 3099	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3082

This theorem is used by:  ralimiaa  3103  ralimi  3104  rr19.3v  3628  rr19.28v  3629  exfo  7104  ffvresb  7125  f1mpt  7261  weniso  7360  xpord2indlem  8145  ixpf  8920  ixpiunwdom  9555  tz9.12lem3  9764  dfac2a  10125  kmlem12  10157  axdc2lem  10443  ac6c4  10476  brdom6disj  10527  konigthlem  10564  arch  12512  cshw1  14878  serf0  15751  symgextfo  19515  baspartn  23140  ptcnplem  23807  spanuni  31925  lnopunilem1  32391  phpreu  38288  finixpnum  38289  poimirlem26  38330  indexa  38417  heiborlem5  38499  rngmgmbs4  38615  mzpincl  43498  dfac11  43822  mnurndlem1  45024  natlocalincr  47625  stgoldbwt  48574  2zrngnmlid2  49055