Theorem ralimia 3086

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3067

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

This theorem depends on definitions:  df-bi 207  df-ral 3068

This theorem is referenced by:  ralimiaa  3088  ralimi  3089  rr19.3v  3680  rr19.28v  3681  exfo  7139  ffvresb  7159  f1mpt  7298  weniso  7390  xpord2indlem  8188  ixpf  8978  ixpiunwdom  9659  tz9.12lem3  9858  dfac2a  10199  kmlem12  10231  axdc2lem  10517  ac6c4  10550  brdom6disj  10601  konigthlem  10637  arch  12550  cshw1  14870  serf0  15729  symgextfo  19464  baspartn  22982  ptcnplem  23650  spanuni  31576  lnopunilem1  32042  phpreu  37564  finixpnum  37565  poimirlem26  37606  indexa  37693  heiborlem5  37775  rngmgmbs4  37891  mzpincl  42690  dfac11  43019  mnurndlem1  44250  natlocalincr  46795  stgoldbwt  47650  2zrngnmlid2  47980