Theorem ralimia 3078

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

Syntax hints:   → wi 4   ∈ wcel 2104  ∀wral 3059

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 206  df-ral 3060

This theorem is referenced by:  ralimiaa  3080  ralimi  3081  rr19.3v  3656  rr19.28v  3657  exfo  7105  ffvresb  7125  f1mpt  7262  weniso  7353  xpord2indlem  8135  ixpf  8916  ixpiunwdom  9587  tz9.12lem3  9786  dfac2a  10126  kmlem12  10158  axdc2lem  10445  ac6c4  10478  brdom6disj  10529  konigthlem  10565  arch  12473  cshw1  14776  serf0  15631  symgextfo  19331  baspartn  22677  ptcnplem  23345  spanuni  31064  lnopunilem1  31530  phpreu  36775  finixpnum  36776  poimirlem26  36817  indexa  36904  heiborlem5  36986  rngmgmbs4  37102  mzpincl  41774  dfac11  42106  mnurndlem1  43342  natlocalincr  45888  stgoldbwt  46742  2zrngnmlid2  46937