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 2106  ∀wral 3061

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

This theorem depends on definitions:  df-bi 206  df-ral 3062

This theorem is referenced by:  ralimiaa  3082  ralimi  3083  rr19.3v  3656  rr19.28v  3657  exfo  7103  ffvresb  7120  f1mpt  7256  weniso  7347  xpord2indlem  8129  ixpf  8910  ixpiunwdom  9581  tz9.12lem3  9780  dfac2a  10120  kmlem12  10152  axdc2lem  10439  ac6c4  10472  brdom6disj  10523  konigthlem  10559  arch  12465  cshw1  14768  serf0  15623  symgextfo  19284  baspartn  22448  ptcnplem  23116  spanuni  30784  lnopunilem1  31250  phpreu  36460  finixpnum  36461  poimirlem26  36502  indexa  36589  heiborlem5  36671  rngmgmbs4  36787  mzpincl  41457  dfac11  41789  mnurndlem1  43025  natlocalincr  45576  stgoldbwt  46430  2zrngnmlid2  46802