Theorem ralimia 3095

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

Syntax hints:   → wi 4   ∈ wcel 2141  ∀wral 3075

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

This theorem depends on definitions:  df-bi 209  df-ral 3076

This theorem is referenced by:  ralimiaa  3097  ralimi  3098  rr19.3v  3625  rr19.28v  3626  exfo  7081  ffvresb  7102  f1mpt  7240  weniso  7333  xpord2indlem  8121  ixpf  8896  ixpiunwdom  9532  tz9.12lem3  9741  dfac2a  10080  kmlem12  10112  axdc2lem  10399  ac6c4  10432  brdom6disj  10483  konigthlem  10520  arch  12472  cshw1  14829  serf0  15699  symgextfo  19453  baspartn  23002  ptcnplem  23669  spanuni  31704  lnopunilem1  32170  phpreu  38064  finixpnum  38065  poimirlem26  38106  indexa  38193  heiborlem5  38275  rngmgmbs4  38391  mzpincl  43276  dfac11  43600  mnurndlem1  44818  natlocalincr  47413  stgoldbwt  48359  2zrngnmlid2  48840