Theorem ralimia 3077

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

Syntax hints:   → wi 4   ∈ wcel 2105  ∀wral 3058

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

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

This theorem is referenced by:  ralimiaa  3079  ralimi  3080  rr19.3v  3666  rr19.28v  3667  exfo  7124  ffvresb  7144  f1mpt  7280  weniso  7373  xpord2indlem  8170  ixpf  8958  ixpiunwdom  9627  tz9.12lem3  9826  dfac2a  10167  kmlem12  10199  axdc2lem  10485  ac6c4  10518  brdom6disj  10569  konigthlem  10605  arch  12520  cshw1  14856  serf0  15713  symgextfo  19454  baspartn  22976  ptcnplem  23644  spanuni  31572  lnopunilem1  32038  phpreu  37590  finixpnum  37591  poimirlem26  37632  indexa  37719  heiborlem5  37801  rngmgmbs4  37917  mzpincl  42721  dfac11  43050  mnurndlem1  44276  natlocalincr  46829  stgoldbwt  47700  2zrngnmlid2  48100