Theorem ralimia 3071

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3051

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 207  df-ral 3052

This theorem is referenced by:  ralimiaa  3073  ralimi  3074  rr19.3v  3609  rr19.28v  3610  exfo  7057  ffvresb  7078  f1mpt  7216  weniso  7309  xpord2indlem  8097  ixpf  8868  ixpiunwdom  9505  tz9.12lem3  9713  dfac2a  10052  kmlem12  10084  axdc2lem  10370  ac6c4  10403  brdom6disj  10454  konigthlem  10491  arch  12434  cshw1  14784  serf0  15643  symgextfo  19397  baspartn  22919  ptcnplem  23586  spanuni  31615  lnopunilem1  32081  phpreu  37925  finixpnum  37926  poimirlem26  37967  indexa  38054  heiborlem5  38136  rngmgmbs4  38252  mzpincl  43166  dfac11  43490  mnurndlem1  44708  natlocalincr  47306  stgoldbwt  48252  2zrngnmlid2  48733