Theorem ralimia 3105

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

Syntax hints:   → wi 4   ∈ wcel 2149  ∀wral 3085

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

This theorem depends on definitions:  df-bi 210  df-ral 3086

This theorem is referenced by:  ralimiaa  3107  ralimi  3108  rr19.3v  3635  rr19.28v  3636  exfo  7098  ffvresb  7119  f1mpt  7257  weniso  7350  xpord2indlem  8139  ixpf  8914  ixpiunwdom  9548  tz9.12lem3  9757  dfac2a  10109  kmlem12  10141  axdc2lem  10428  ac6c4  10461  brdom6disj  10512  konigthlem  10549  arch  12497  cshw1  14855  serf0  15728  symgextfo  19488  baspartn  23076  ptcnplem  23743  spanuni  31833  lnopunilem1  32299  phpreu  38138  finixpnum  38139  poimirlem26  38180  indexa  38267  heiborlem5  38349  rngmgmbs4  38465  mzpincl  43350  dfac11  43674  mnurndlem1  44876  natlocalincr  47477  stgoldbwt  48423  2zrngnmlid2  48904